SetLike.coe_mem
theorem SetLike.coe_mem : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} (x : ↥p), ↑x ∈ p
This theorem states that for any types `A` and `B`, and a set-like structure `i` on `A` and `B`, given a set `p` of type `A` and an element `x` of type `↥p` (which means `x` is an element of `p`), the coercion of `x` back into type `B` (denoted by `↑x`) is an element of `p`. Essentially, it says that if `x` is an element of `p`, then `x` remains an element of `p` even after it is converted to `B`.
More concisely: For any set-like structures `i` on types `A` and `B`, and a set `p` of type `A`, the coercion of an element `x` of type `A` belonging to `p` back into type `B` (denoted by `↑x`) also belongs to `p`.
|
SetLike.forall
theorem SetLike.forall :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : ↥p → Prop},
(∀ (x : ↥p), q x) ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, h⟩
This theorem expresses a property of set-like structures. For any types `A` and `B`, and a set-like relationship `i` between `A` and `B`, the theorem says that for a particular `p` of type `A` and a property `q` that applies to elements of `p`, the statement "for all elements `x` of `p`, `q` holds for `x`" is equivalent to "for all `x` of type `B` such that `x` is in `p`, `q` holds for `x`, given the context that `x` is in `p`." This provides a way to express a universal quantification over elements of a subset in terms of a universal quantification over elements of the containing set.
More concisely: For any set-like relationship between types `A` and `B` and property `q`, the statement "for all `x` in `A`, `q(x)` holds if and only if for all `y` in `B` such that `y` is in `A`, `q(y)` holds.
|
Mathlib.Data.SetLike.Basic._auxLemma.3
theorem Mathlib.Data.SetLike.Basic._auxLemma.3 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : B}, (x ∈ ↑p) = (x ∈ p)
This theorem states that for any types `A` and `B`, given a `SetLike` instance `i` between `A` and `B`, and for any object `p` of type `A` and `x` of type `B`, the statement "`x` is in the set corresponding to `p`" is equivalent to the statement "`x` is in `p`". In mathematical terms, if `A` and `B` are sets and `p` is an element of `A`, then `x` belonging to the set corresponding to `p` is the same as `x` belonging to `p`.
More concisely: For any type `A` and `B`, and for any `SetLike` instance `i` between them, and for any `p : A` and `x : B`, `x ∈ i.toSet p` if and only if `x ∈ p`.
|
Mathlib.Data.SetLike.Basic._auxLemma.5
theorem Mathlib.Data.SetLike.Basic._auxLemma.5 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} (x : ↥p), (↑x ∈ p) = True
This theorem states that for any types `A` and `B`, if `A` behaves like a set of `B` (as specified by the `SetLike A B` type class), and for any element `p` of type `A` and `x` of the subtype of `A` defined by `p`, the statement "`x` belongs to `p`" is always true. In other words, if `x` is an element of a set-like `A` object `p`, then `x` is indeed an element of `p`.
More concisely: For any set-like type `A` and element `p` of type `A`, any subelement `x` of `p` belongs to `p`.
|
SetLike.coe_injective'
theorem SetLike.coe_injective' :
∀ {A : Type u_1} {B : outParam (Type u_2)} [self : SetLike A B], Function.Injective SetLike.coe
The theorem `SetLike.coe_injective'` states that for any types `A` and `B` where `A` behaves like a set of `B`, the function that coerces (or converts) a term of `A` into a set of `B` is injective. In other words, if two elements of `A` are mapped to the same set of `B` via this coercion, then those two elements of `A` are actually the same. This injectivity property ensures that no information is lost during the conversion from `A` to a set of `B`.
More concisely: If `A` and `B` are types with `A` behaving like a set of `B`, then the coercion function from `A` to the set of `B` is an injection.
|
SetLike.not_le_iff_exists
theorem SetLike.not_le_iff_exists :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, ¬p ≤ q ↔ ∃ x ∈ p, x ∉ q
This theorem states that for any two sets 'p' and 'q' of a type 'A' that behaves like a set of a type 'B', 'p' is not a subset of 'q' if and only if there exists an element 'x' in 'p' that is not in 'q'. Here, 'SetLike A B' is a typeclass assumption which means 'A' behaves like a 'set' over 'B'. The '≤' operator denotes subset or substructure relationship in this context.
More concisely: For sets 'p' and 'q' of type 'A' that have the set behavior over 'B', 'p' is strictly subset of 'q' if and only if there is no element in 'p' that is in 'q'.
|
SetLike.ext'_iff
theorem SetLike.ext'_iff : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p = q ↔ ↑p = ↑q
This theorem, `SetLike.ext'_iff`, states that for any two types `A` and `B`, where `A` is set-like over `B`, and for any two elements `p` and `q` of type `A`, `p` is equal to `q` if and only if the set-like coercions of `p` and `q` to `B` are equal. In simpler terms, it means that if we have a type `A` that behaves like a set of elements of another type `B`, two instances of `A` are equal if their corresponding "sets" of `B` elements are equal.
More concisely: For set-like types `A` over `B`, two elements `p` and `q` of `A` are equal if and only if their set-like coercions to `B` are equal.
|
SetLike.mem_coe
theorem SetLike.mem_coe : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ p
This theorem states that for any types `A` and `B`, and any instance of `SetLike A B`, the membership of an element `x` of type `B` in the coercion of an object `p` of type `A` is equivalent to the membership of `x` in `p`. In other words, if we have a type that behaves like a set, coercing it to a set doesn't change whether a particular element belongs to it.
More concisely: For any types `A`, `B` and instance of `SetLike A B`, the membership `x ∈ p` holds if and only if `x ∈ (coe : A → Set) p`.
|
SetLike.coe_subset_coe
theorem SetLike.coe_subset_coe : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {S T : A}, ↑S ⊆ ↑T ↔ S ≤ T := by
sorry
The theorem `SetLike.coe_subset_coe` establishes a connection between the subset relation and the less-than-or-equal-to relation for set-like objects. Specifically, for any two types `A` and `B` with `A` being set-like over `B`, and any two elements `S` and `T` of type `A`, `S` is a subset of `T` if and only if `S` is less-than-or-equal-to `T`, where the subset relation is defined in the context of the coe function (which coerces `S` and `T` to be sets).
More concisely: For set-like objects `A` over `B` and `S` and `T` in `A`, `S ⊆ T` if and only if `S ≤ T` as sets, where `≤` is the subset relation defined via the coe function.
|
SetLike.ext
theorem SetLike.ext : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, (∀ (x : B), x ∈ p ↔ x ∈ q) → p = q
The theorem `SetLike.ext` states that for any two objects `p` and `q` of type `A`, which has a `SetLike` relationship with type `B`, if for every `x` of type `B`, `x` belongs to `p` if and only if `x` belongs to `q`, then `p` is equal to `q`. In other words, two `SetLike` objects are considered equal if they contain exactly the same elements. Note that implementers of `SetLike` must reproduce this lemma in their code and tag it with `@[ext]`.
More concisely: If two `SetLike` objects `p` and `q` over type `A` with respect to type `B` have equal elements, then `p` is equal to `q`.
|
SetLike.lt_iff_le_and_exists
theorem SetLike.lt_iff_le_and_exists :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p
This theorem is stating a condition for one set-like object to be less than another. Specifically, within the context of any two types `A` and `B` with a `SetLike` relationship, it holds that for any two instances `p` and `q` of type `A`, `p` is less than `q` if and only if `p` is less than or equal to `q` and there exists an element `x` in `q` that is not in `p`.
More concisely: For any set-like types `A` and `B` and instances `p` of `A` and `q` of `B`, `p` is less than `q` if and only if `p` is subset of `q` and there exists an element in `q` not in `p`.
|
Mathlib.Data.SetLike.Basic._auxLemma.4
theorem Mathlib.Data.SetLike.Basic._auxLemma.4 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x y : ↥p}, (↑x = ↑y) = (x = y)
This theorem states that for any types `A` and `B`, given that `A` is a "set-like" structure over `B`, and for any element `p` of type `A` and elements `x` and `y` which are of the type of elements of `p`, the equality of the coerced values of `x` and `y` (when they are treated as elements of the underlying set `B`) is equivalent to the equality of `x` and `y` themselves. This asserts the consistency of equality when transitioning between the "set-like" structure and the underlying set.
More concisely: For any set-like structure `A` over type `B`, and for all `a : A` and `x, y : elem a`, if `x = y` in `A`, then `x = y` in `B`.
|
SetLike.ext'
theorem SetLike.ext' : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, ↑p = ↑q → p = q
This theorem states that for any two types `A` and `B`, given that `A` is a "set-like" type of `B`, if two elements `p` and `q` of type `A` have the same interpretations as elements of type `B` (i.e., `↑p = ↑q`), then `p` and `q` must be the same elements of type `A` (i.e., `p = q`). In other words, this theorem asserts that the interpretation function in the `SetLike` typeclass is injective (or one-to-one).
More concisely: Given two set-like types `A` and `B` with `A` being set-like over `B`, if for all `p, q ∈ A`, `↑p = ↑q` implies `p = q`, then the interpretation function `↑ : A → B` is injective.
|
SetLike.ext_iff
theorem SetLike.ext_iff :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p = q ↔ ∀ (x : B), x ∈ p ↔ x ∈ q
This theorem states that for any types `A` and `B`, given a `SetLike` instance `i` between `A` and `B`, and any two elements `p` and `q` of type `A`, `p` is equal to `q` if and only if for every element `x` of type `B`, `x` is an element of `p` if and only if `x` is an element of `q`. In other words, two sets are equal if and only if they contain exactly the same elements.
More concisely: Two sets `A` and `B` are equal if and only if for all elements `x`, `x` is in `A` if and only if `x` is in `B`.
|
SetLike.exists_of_lt
theorem SetLike.exists_of_lt : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, p < q → ∃ x ∈ q, x ∉ p := by
sorry
This theorem states that for any two types `A` and `B`, if `A` is a set-like structure of `B`, and `p` and `q` are elements of `A` such that `p` is less than `q`, then there exists an element `x` that belongs to `q` but does not belong to `p`. In other words, if `A` is a set-like structure and one element of this structure is strictly smaller than another, there must be at least one member in the larger element that is not in the smaller one.
More concisely: For any set-like structure `A` of type `B` in Lean 4, if `p` and `q` are elements of `A` with `p` strictly contained in `q`, then there exists an element `x` in `q` not in `p`.
|
SetLike.coe_mono
theorem SetLike.coe_mono : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B], Monotone SetLike.coe
The theorem `SetLike.coe_mono` states that for all types `A` and `B`, where `A` is a `SetLike` of `B`, the function `SetLike.coe` (which is a coercion from a term of `A` to its corresponding `Set`) is monotone. In other words, given a partial order on `A` and `B`, if `a` and `b` are two elements in `A` such that `a ≤ b`, then the corresponding sets obtained by the coercion function from `a` and `b` also satisfy `SetLike.coe a ≤ SetLike.coe b`.
More concisely: For any type `A` being a `SetLike` of `B` and given a partial order on `A`, if `a ≤ b` in `A`, then `SetLike.coe (a : Set B) ≤ SetLike.coe (b : Set B)` in the lattice of sets.
|
SetLike.coe_set_eq
theorem SetLike.coe_set_eq : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, ↑p = ↑q ↔ p = q
This theorem, `SetLike.coe_set_eq`, states that for any two types `A` and `B`, and a `SetLike` instance `i` from `A` to `B`, the two instances `p` and `q` of type `A` are equal if and only if their coercions to type `B` are equal. In other words, it describes the equivalence between equality of two objects of a certain type and the equality of their corresponding objects under a certain `SetLike` mapping.
More concisely: For any type `A`, `B`, and `SetLike` instance `i` from `A` to `B`, `a = b` if and only if `i a = i b`.
|
SetLike.le_def
theorem SetLike.le_def :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {S T : A}, S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T
This theorem, `SetLike.le_def`, relates to the notion of set-like structures in Lean 4, specifically those of type `A` that can be treated as though they were sets of type `B`. It states that for any two such structures `S` and `T`, `S` is less than or equal to `T` if and only if every element `x` of type `B` that belongs to `S` also belongs to `T`.
More concisely: For set-like structures `S` and `T` of types `A` and `B` respectively, `S ≤T` if and only if for all `x:B`, `x ∈ S` implies `x ∈ T`.
|
Mathlib.Data.SetLike.Basic._auxLemma.6
theorem Mathlib.Data.SetLike.Basic._auxLemma.6 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {S T : A}, (↑S ⊆ ↑T) = (S ≤ T)
This theorem, `Mathlib.Data.SetLike.Basic._auxLemma.6`, states that for any two types `A` and `B`, given a `SetLike` instance `i` between `A` and `B`, and any two elements `S` and `T` of type `A`, the statement that the coercion of `S` is a subset of the coercion of `T` (expressed as `↑S ⊆ ↑T`) is equivalent to the statement that `S` is less than or equal to `T` (expressed as `S ≤ T`). Here, the `SetLike` instance provides a way to treat elements of `A` like sets, and `↑` is a coercion operator that turns elements of `A` into sets. The theorem expresses a fundamental property of ordered structures where the subset relation corresponds to the order relation.
More concisely: For any type `A` with a `SetLike` instance and coercion `↑`, the statement `↑S ⊆ ↑T` is equivalent to `S ≤ T`.
|
SetLike.coe_injective
theorem SetLike.coe_injective : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B], Function.Injective SetLike.coe := by
sorry
The theorem `SetLike.coe_injective` states that for any types `A` and `B`, given an instance of `SetLike A B`, the coercion function `SetLike.coe` is injective. In other words, if `SetLike.coe` applied to two different elements of type `A` gives the same set of type `B`, then the two elements of type `A` were actually the same. In mathematical terms, if `SetLike.coe a1 = SetLike.coe a2`, then `a1 = a2`. This theorem ensures the uniqueness of elements in the `SetLike` structure when mapped to their corresponding set.
More concisely: Given types `A` and `B` with an instance of `SetLike A B`, `SetLike.coe` is an injection from `A` to the sets represented by elements of type `B`.
|