Pairwise.set_pairwise
theorem Pairwise.set_pairwise : ∀ {α : Type u_1} {r : α → α → Prop}, Pairwise r → ∀ (s : Set α), s.Pairwise r := by
sorry
The theorem `Pairwise.set_pairwise` states that for any type `α` and a given relation `r` that is pairwise, if we have a set `s` of type `α`, then the relation `r` is pairwise on the set `s`. In other words, for any two distinct elements `x` and `y` in the set `s`, the relation `r` holds between `x` and `y`. This implies that if a relation holds pairwise across the entire type, it will also hold pairwise for any subset of that type.
More concisely: If `r` is a pairwise relation on type `α`, then `r` holds between any two distinct elements in any set `s` of type `α`.
|
Function.Injective.pairwise_ne
theorem Function.Injective.pairwise_ne :
∀ {α : Type u_1} {ι : Type u_4} {f : ι → α}, Function.Injective f → Pairwise ((fun x x_1 => x ≠ x_1) on f) := by
sorry
The theorem `Function.Injective.pairwise_ne` states that for any types `α` and `ι`, and any function `f` from `ι` to `α`, if `f` is injective, then the relation `x ≠ x_1` holds pairwise when applied to `f`. In other words, if `f` is such that it always produces a different output for different inputs, then for any two distinct elements in the domain of `f`, their images under `f` are also distinct.
More concisely: If `f` is a function from type `ι` to type `α` that is injective, then for all distinct `x` and `x_1` in `ι`, `f x ≠ f x_1`.
|
Pairwise.mono
theorem Pairwise.mono : ∀ {α : Type u_1} {r p : α → α → Prop}, Pairwise r → (∀ ⦃i j : α⦄, r i j → p i j) → Pairwise p
The theorem `Pairwise.mono` states that for any type `α` and any two relations `r` and `p` on `α`, if the relation `r` holds pairwise and for all `i` and `j` in `α`, if `r i j` implies `p i j`, then the relation `p` also holds pairwise. In other words, if we have a pairwise relation `r` and every instance of `r` implies an instance of another relation `p`, then `p` is also pairwise.
More concisely: If a relation `r` on a type `α` is pairwise and implies another relation `p` on `α` pairwise, then `p` is pairwise.
|
Set.Pairwise.eq
theorem Set.Pairwise.eq :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a b : α}, s.Pairwise r → a ∈ s → b ∈ s → ¬r a b → a = b
This theorem states that for any type `α`, any relation `r` on `α`, any set `s` of elements of type `α`, and any two elements `a` and `b` of type `α`, if the relation `r` holds pairwise on the set `s` (meaning, for every pair of distinct elements in `s`, `r` holds), and both `a` and `b` are elements of `s`, and the relation `r` does not hold for `a` and `b`, then `a` and `b` must be equal.
More concisely: If `α` is a type, `r` is a relation on `α`, `s` is a set of distinct elements of `α`, and for all `a, b ∈ s`, `a` and `b` relate under `r` implies `a = b`, then every pair of distinct elements `a, b ∈ s` that do not relate under `r` must be equal.
|
Set.Pairwise.imp
theorem Set.Pairwise.imp :
∀ {α : Type u_1} {r p : α → α → Prop} {s : Set α}, s.Pairwise r → (∀ ⦃a b : α⦄, r a b → p a b) → s.Pairwise p := by
sorry
This theorem states that for any type `α`, two relations `r` and `p` on `α`, and a set `s` of elements from `α`, if the relation `r` holds pairwise on the set `s` and every pair in which `r` holds implies `p` holds, then the relation `p` also holds pairwise on the set `s`. In other words, if `r` is a stronger relation than `p` and `r` holds for all distinct pairs in the set `s`, then `p` also holds for all distinct pairs in the set `s`.
More concisely: If `r` is a transitive relation on type `α` that holds between all distinct elements in `s`, and `r` implies `p`, then `p` is also a relation that holds pairwise between all distinct elements in `s`.
|