HasSSubset.SSubset.ne
theorem HasSSubset.SSubset.ne :
∀ {α : Type u} [inst : HasSSubset α] [inst_1 : IsIrrefl α fun x x_1 => x ⊂ x_1] {a b : α}, a ⊂ b → a ≠ b
This theorem, named `HasSSubset.SSubset.ne`, states that for any type `α` that has a subset structure and respects the property of irreflexivity (meaning that no element is considered a proper subset of itself), if `a` and `b` are elements of `α` such that `a` is a proper subset of `b` (symbolized as `a ⊂ b`), then `a` and `b` must be distinct, i.e., `a` is not equal to `b`.
More concisely: If `α` is a type with irreflexive subset structure, then for all `a` and `b` in `α`, if `a` is a proper subset of `b` (`a ⊂ b`), then `a ≠ b`.
|
IsWellFounded.induction
theorem IsWellFounded.induction :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] {C : α → Prop} (a : α),
(∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a
The theorem `IsWellFounded.induction` states that for any type `α` and a well-founded relation `r` on `α`, given a property `C` and an element `a` of type `α`, if for all `x` of type `α`, the property `C` holds for `x` if `C` holds for all `y` such that `r y x`, then the property `C` holds for `a`. This is essentially an induction principle for well-founded relations, allowing us to prove properties about elements of a well-founded set by considering smaller elements first.
More concisely: If `r` is a well-founded relation on type `α`, then for any property `C` and element `a` of type `α`, if `C` holds for all `x` such that `r x a`, then `C` holds for `a`.
|
right_iff_left_not_left
theorem right_iff_left_not_left :
∀ {α : Type u} {r s : α → α → Prop} [inst : IsNonstrictStrictOrder α r s] {a b : α}, s a b ↔ r a b ∧ ¬r b a := by
sorry
This theorem named `right_iff_left_not_left` states that for any type `α` and any two relations `r` and `s` on `α`, assuming that `r` and `s` form a nonstrict strict order, for any two elements `a` and `b` of type `α`, `s a b` is true if and only if `r a b` is true and `r b a` is not true. In other words, this theorem provides a characterization of the relation `s` in terms of the relation `r` under the assumption that `r` and `s` form a certain kind of ordered pair.
More concisely: For any type `α` and relations `r` and `s` on `α` forming a nonstrict strict order, `s a b` if and only if `r a b` and not `r b a`.
|
HasSSubset.SSubset.asymm
theorem HasSSubset.SSubset.asymm :
∀ {α : Type u} [inst : HasSSubset α] [inst_1 : IsAsymm α fun x x_1 => x ⊂ x_1] {a b : α}, a ⊂ b → ¬b ⊂ a
This theorem, which is an alias of `ssubset_asymm`, states that for any type `α` that has a "strict subset" relation (denoted as `⊂`), and this relation is asymmetric, then for any two elements `a` and `b` of type `α`, if `a` is a strict subset of `b`, then `b` cannot be a strict subset of `a`. In other words, the "strict subset" relationship cannot go both ways between two elements, reflecting the asymmetry of this relation.
More concisely: If `α` is a type with an asymmetric strict subset relation (`⊂`), then for all `a` and `b` in `α`, if `a ⊂ b`, then `b ⊂ a` implies `a = b`.
|
IsTrichotomous.swap
theorem IsTrichotomous.swap :
∀ {α : Type u} (r : α → α → Prop) [inst : IsTrichotomous α r], IsTrichotomous α (Function.swap r)
The theorem `IsTrichotomous.swap` states that for any type `α` and a relation `r : α → α → Prop` such that `r` is trichotomous, the function `Function.swap r`, which reverses the order of the arguments of `r`, is also trichotomous. In mathematical terms, a relation is trichotomous if for any two elements `a` and `b` of type `α`, exactly one of the following is true: `r a b`, `r b a` or `a = b`. Thus, the theorem is saying that reversing the order of arguments doesn't affect the trichotomous property of the relation.
More concisely: If `r : α → α → Prop` is a trichotomous relation, then `Function.swap r` is also a trichotomous relation.
|
HasSubset.Subset.eq_or_ssubset
theorem HasSubset.Subset.eq_or_ssubset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → a = b ∨ a ⊂ b
This theorem, termed as an alias of `eq_or_ssubset_of_subset`, states that for any type `α` that has a subset and strict subset operation, and for which a nonstrict-strict order and antisymmetry is defined in terms of these operations, given any two elements `a` and `b` of type `α`, if `a` is a subset of `b`, then `a` is either equal to `b` or is a strict subset of `b`.
More concisely: If `a` is a subset of `b` in a type `α` with subset and strict subset operations and a defined nonstrict-strict order and antisymmetry, then `a` is equal to `b` or is a strict subset of `b`.
|
subset_of_ssubset
theorem subset_of_ssubset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}, a ⊂ b → a ⊆ b
This theorem, `subset_of_ssubset`, states that for any type `α` that has a subset operation and a strict subset operation, and where these operations form a nonstrict-strict order, if `a` is a strict subset of `b` (denoted as `a ⊂ b`), then `a` is also a subset of `b` (denoted as `a ⊆ b`). This is a basic property of set theory, reflecting the intuitive idea that if a set `a` is strictly contained within another set `b`, then naturally every element in `a` is also present in `b`.
More concisely: If `a` strictly contains `b`, then `a` is a subset of `b`. (In mathematical notation: `a ⊂ b` implies `a ⊆ b`.))
|
IsWellFounded.apply
theorem IsWellFounded.apply : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] (a : α), Acc r a
This theorem states that for any type `α` and any relation `r` on `α`, if the relation `r` is well-founded on `α` (as indicated by the typeclass instance `IsWellFounded α r`), then every element `a` of type `α` is accessible under the relation `r`. In mathematical terms, the accessibility of an element `a` under the relation `r` means that there is no infinite descending sequence (i.e., a sequence `a, b, c, ...,` such that `r(b, a)`, `r(c, b)`, and so on) starting at `a`.
More concisely: If `α` is a type and `r` is a well-founded relation on `α` (`IsWellFounded α r`), then every element of `α` is accessible under `r`, i.e., there is no infinite descending sequence starting at any element.
|
subset_trans
theorem subset_trans :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : IsTrans α fun x x_1 => x ⊆ x_1] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ c
This theorem, `subset_trans`, states that for any type `α` that has a subset operation and a transitive relation, if `a`, `b`, and `c` are elements of `α`, and `a` is a subset of `b` and `b` is a subset of `c`, then `a` is a subset of `c`. This is a formalization of the transitivity property for subset relationships.
More concisely: If `a` is a subset of `b` and `b` is a subset of `c`, then `a` is a subset of `c`.
|
superset_of_eq
theorem superset_of_eq :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1], a = b → b ⊆ a
This theorem states that for any type `α` that has a subset operation, and any two elements `a` and `b` of this type, if reflexivity property holds for the subset operation (i.e., any element is a subset of itself), then if `a` is equal to `b`, `b` is a subset of `a`. In mathematical terms, for any set `α`, any two elements `a` and `b` of `α`, if `a = b`, then `b` is a subset of `a`.
More concisely: If `α` is a type with a subset operation and reflexivity holds, then for all `a` and `b` in `α`, `a = b` implies `b ⊆ a`.
|
HasSSubset.SSubset.trans_subset
theorem HasSSubset.SSubset.trans_subset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b c : α}
[inst_3 : IsTrans α fun x x_1 => x ⊆ x_1], a ⊂ b → b ⊆ c → a ⊂ c
This theorem, which is also known as an alias of `ssubset_of_ssubset_of_subset`, states that for any type `α` with a subset and strict subset relation, and the subset relation is a non-strict strict order and transitive, if a strict subset relation exists from `a` to `b` and a subset relation exists from `b` to `c`, then a strict subset relation exists from `a` to `c`. In the context of set theory, this theorem describes the transitivity of strict subset relationships under the condition of a subset relationship.
More concisely: If `a ⊂ b` and `b ⊂ c`, then `a ⊂ c` (in a type `α` with transitive and non-reflexive subset relation).
|
HasSubset.Subset.trans
theorem HasSubset.Subset.trans :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : IsTrans α fun x x_1 => x ⊆ x_1] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ c
This theorem, named `HasSubset.Subset.trans`, is an alias for `subset_trans`. It states that for any type `α` that has a subset operation (`HasSubset α`) and in which this subset relation is transitive (`IsTrans α fun x x_1 => x ⊆ x_1`), if `a` is a subset of `b` and `b` is a subset of `c`, then `a` is a subset of `c`. In other words, the subset relationship is transitive: if `a` is included in `b`, and `b` is included in `c`, then `a` must be included in `c`.
More concisely: For types `α` with transitive subset relation, if `a ⊆ b` and `b ⊆ c`, then `a ⊆ c`.
|
HasSSubset.SSubset.trans_eq
theorem HasSSubset.SSubset.trans_eq : ∀ {α : Type u} [inst : HasSSubset α] {a b c : α}, a ⊂ b → b = c → a ⊂ c := by
sorry
This theorem, called `HasSSubset.SSubset.trans_eq`, states that for any type `α` that has a subset operation (`HasSSubset α`), if `a` is a strict subset of `b` (`a ⊂ b`), and `b` is equal to `c` (`b = c`), then `a` is a strict subset of `c` (`a ⊂ c`). Essentially, it allows for transitivity in strict subset relations given equality of two sets.
More concisely: If `a ⊂ b` and `b = c`, then `a ⊂ c` for any type `α` with a defined subset operation (`HasSSubset α`).
|
WellFoundedGT.apply
theorem WellFoundedGT.apply :
∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedGT α] (a : α), Acc (fun x x_1 => x > x_1) a
This theorem states that for any type `α` with a less-than operation and a well-founded greater-than relation, every value `a` of type `α` is accessible under the well-founded greater-than relation. In other words, the theorem confirms that each element in this type `α` participates in a chain of comparisons where each successive element is greater than the previous one, respecting the well-founded principle. This principle ensures that there are no infinite descending chains, which is a key property in well-ordering concepts and induction reasoning.
More concisely: Every element in a type equipped with a well-founded ordering relation has an accessible predecessor under that relation.
|
IsOrderConnected.conn
theorem IsOrderConnected.conn :
∀ {α : Type u} {lt : α → α → Prop} [self : IsOrderConnected α lt] (a b c : α), lt a c → lt a b ∨ lt b c
This theorem states that for any connected order, which is defined as an order that satisfies the condition `a < c implies a < b or b < c`, given any three elements `a`, `b`, and `c` from the ordered set, if `a` is less than `c`, then either `a` is less than `b` or `b` is less than `c`. Here, `α` is the type of the elements in the order, `lt` is the order relation, and `IsOrderConnected α lt` is the property of being a connected order for the type `α` with the relation `lt`.
More concisely: In a connected order `(α, lt)`, if `a lt c` then `a lt b` or `b lt c`.
|
IsNonstrictStrictOrder.right_iff_left_not_left
theorem IsNonstrictStrictOrder.right_iff_left_not_left :
∀ {α : Type u_1} {r : semiOutParam (α → α → Prop)} {s : α → α → Prop} [self : IsNonstrictStrictOrder α r s]
(a b : α), s a b ↔ r a b ∧ ¬r b a
This theorem states that for a given type `α` and two relations `r` and `s` on `α`, if `r` is the nonstrict relation corresponding to the strict relation `s`, then for any two elements `a` and `b` of `α`, `s a b` holds if and only if `r a b` holds and `r b a` does not hold. In other words, `s` is a strict ordering if `a` is related to `b` through `r`, but not vice versa.
More concisely: For relations `r` and `s` on type `α`, `s` is the strictification of `r` if and only if for all `a` and `b` in `α`, `s a b` holds if and only if `r a b` holds and `r b a` does not hold.
|
Eq.trans_ssubset
theorem Eq.trans_ssubset : ∀ {α : Type u} [inst : HasSSubset α] {a b c : α}, a = b → b ⊂ c → a ⊂ c
This theorem, `Eq.trans_ssubset`, states for any type `α` (which has a strict subset operation) and any three elements `a`, `b`, and `c` of this type, if `a` is equal to `b` and `b` is a strict subset of `c`, then `a` is also a strict subset of `c`. In essence, it allows strict subset relations to be transitive over an equality, much like how equality is usually transitive.
More concisely: If `a` equals `b` and `b` is a strict subset of `c`, then `a` is a strict subset of `c`.
|
subset_antisymm_iff
theorem subset_antisymm_iff :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1]
[inst_2 : IsAntisymm α fun x x_1 => x ⊆ x_1], a = b ↔ a ⊆ b ∧ b ⊆ a
This theorem states that for any type 'α' that has a subset operation, given any two elements 'a' and 'b' from this type, if the subset operation is reflexive and antisymmetric, then 'a' is equal to 'b' if and only if 'a' is a subset of 'b' and 'b' is a subset of 'a'. In other words, two elements of a reflexive and antisymmetric subset relation are identical if and only if they are subsets of each other.
More concisely: For any reflexive and antisymmetric subset relation on a type, elements are equal if and only if they are subsets of each other.
|
HasSubset.Subset.trans_ssubset
theorem HasSubset.Subset.trans_ssubset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b c : α}
[inst_3 : IsTrans α fun x x_1 => x ⊆ x_1], a ⊆ b → b ⊂ c → a ⊂ c
This is a theorem about subset relationships in the context of nonstrict and strict orders, specifically, it is a "transitivity" rule for such orders. Given any type `α` with a subset `⊆` and a strict subset `⊂` relationship, and assuming that the subset `⊆` relationship obeys the transitivity property, if `a` is a subset of `b` and `b` is a strict subset of `c`, then `a` is a strict subset of `c`. This essentially allows us to "chain" subset and strict subset relationships together to deduce a new strict subset relationship.
More concisely: If `a ⊆ b` and `b ⊂ c`, then `a ⊂ c` (in the context of nonstrict and strict subset relationships).
|
HasSubset.Subset.ssubset_of_not_subset
theorem HasSubset.Subset.ssubset_of_not_subset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α},
a ⊆ b → ¬b ⊆ a → a ⊂ b
This theorem, also known as an alias of `ssubset_of_subset_not_subset`, states that for any types `α` where `α` has both a subset and strict subset relationship, and where the subset relationship is a non-strict strict order, if `a` is a subset of `b` and `b` is not a subset of `a`, then `a` is a strict subset of `b`.
More concisely: If $A$ is a subset of $B$ and $B$ is not a subset of $A$, then $A$ is a proper subset of $B$.
|
subset_antisymm
theorem subset_antisymm :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → b ⊆ a → a = b
This theorem, `subset_antisymm`, states that for any type `α` with a subset operation and an antisymmetry property, if `a` and `b` are elements of `α` such that `a` is a subset of `b` and `b` is a subset of `a`, then `a` is equal to `b`. In other words, within a given type that has an antisymmetric subset relation, two elements are equal if and only if they are subsets of each other. This is a formalization of the antisymmetry property of set inclusion in the context of general types in Lean 4.
More concisely: If `α` is a type with an antisymmetric subset relation, then for all `a` and `b` in `α`, `a ⊆ b` and `b ⊆ a` imply `a = b`.
|
HasSubset.Subset.eq_of_not_ssuperset
theorem HasSubset.Subset.eq_of_not_ssuperset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → ¬a ⊂ b → b = a
This theorem, `HasSubset.Subset.eq_of_not_ssuperset`, states that for any type `α` with subset (`⊆`) and strict subset (`⊂`) operations, and assuming the nonstrict-strict order relations between elements of `α` are well-defined, if `a` and `b` are elements of `α` and `α` is antisymmetric under the subset operation, then if `a` is a subset of `b` and `a` is not a strict subset of `b`, it must be that `b` equals `a`. In other words, if `a` is included in `b` and `a` is not properly included in `b` (there doesn't exist any element in `b` that is not in `a`), then `b` and `a` must be the same set.
More concisely: If `α` is an antisymmetric set with subset and strict subset operations, then for all `a, b ∈ α`, if `a ⊆ b` and `a ⊂≠ b`, then `a = b`.
|
HasSubset.subset.trans_eq
theorem HasSubset.subset.trans_eq : ∀ {α : Type u} [inst : HasSubset α] {a b c : α}, a ⊆ b → b = c → a ⊆ c
This theorem, known as an alias of `subset_of_subset_of_eq`, states that for any type `α` that has a subset relation, if `a` is a subset of `b` and `b` equals `c`, then `a` is a subset of `c`. In mathematical terms, for all sets `a`, `b`, and `c`, if `a ⊆ b` and `b = c`, then it follows that `a ⊆ c`.
More concisely: If `a` is a subset of `b` and `b` equals `c`, then `a` is a subset of `c`. In mathematical notation: `a ⊆ b ∧ b = c` implies `a ⊆ c`.
|
HasSubset.Subset.eq_of_not_ssubset
theorem HasSubset.Subset.eq_of_not_ssubset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → ¬a ⊂ b → a = b
This theorem, `HasSubset.Subset.eq_of_not_ssubset`, states that for any type `α` where `α` has a subset and strict subset relationship, and these relationships form a non-strict strict order and are antisymmetric, if `a` is a subset of `b` and `a` is not a strict subset of `b`, then `a` is equal to `b`. In mathematical terms, for sets `a` and `b`, if `a ⊆ b` (a is a subset of b) and it's not the case that `a ⊂ b` (a is not a strict subset of b), then `a = b`.
More concisely: If `α` is a type with a partial order where subset relation is antisymmetric and transitive, and `a` is a subset of `b` but not a strict subset, then `a = b`.
|
extensional_of_trichotomous_of_irrefl
theorem extensional_of_trichotomous_of_irrefl :
∀ {α : Type u} (r : α → α → Prop) [inst : IsTrichotomous α r] [inst : IsIrrefl α r] {a b : α},
(∀ (x : α), r x a ↔ r x b) → a = b
This theorem states that in a trichotomous irreflexive order, any two elements 'a' and 'b' are identical if they have the same set of predecessors. In other words, every element in this type of ordering structure is uniquely determined by the set of elements which precede it. Here, a relation 'r' on a type 'α' is considered trichotomous if for any two elements in 'α', either the first element is related to the second, the second is related to the first, or they are the same. The relation is irreflexive if no element is related to itself.
More concisely: In a trichotomous and irreflexive order, two elements are equal if they have the same set of predecessors.
|
HasSubset.Subset.ssubset_of_ne
theorem HasSubset.Subset.ssubset_of_ne :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → a ≠ b → a ⊂ b
This theorem, aptly named `HasSubset.Subset.ssubset_of_ne`, states the following: Given any type `α` that has a subset and strict subset relations, and these relations form a non-strict strict order on `α` (meaning that the subset relation is reflexive and transitive, and the strict subset relation is irreflexive and transitive), if `a` and `b` are elements of `α` such that the subset relation is also antisymmetric (if `a` is a subset of `b` and `b` is a subset of `a`, then `a` equals `b`), then if `a` is a subset of `b` and `a` is not equal to `b`, it follows that `a` is a strict subset of `b`. In mathematical terms, for any `a` and `b` in `α`, if `a ⊆ b` and `a ≠ b`, then `a ⊂ b`.
More concisely: If `α` is a type with reflexive, transitive subset relation `⊆` and irreflexive, transitive strict subset relation `⊂`, then for all `a, b` in `α`, if `a ⊆ b` and `a ≠ b`, then `a ⊂ b`.
|
IsTrans.swap
theorem IsTrans.swap : ∀ {α : Type u} (r : α → α → Prop) [inst : IsTrans α r], IsTrans α (Function.swap r)
The theorem `IsTrans.swap` states that for any type `α` and a binary relation `r` on `α`, if `r` is transitive, then the swapped variant of `r` is also transitive. Here, a relation `r` is transitive (denoted `IsTrans α r`) if for any three elements `a`, `b`, `c` of type `α`, `r a b` and `r b c` imply `r a c`. The swapped variant of `r` (denoted `Function.swap r`) is a relation that takes two inputs in the opposite order, i.e., if `r` is a relation from `α` to `β`, then `Function.swap r` is a relation from `β` to `α`.
More concisely: If `r` is a transitive relation on type `α`, then the swapped relation `Function.swap r` is also transitive.
|
HasSubset.Subset.ssubset_or_eq
theorem HasSubset.Subset.ssubset_or_eq :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → a ⊂ b ∨ a = b
This theorem, `HasSubset.Subset.ssubset_or_eq`, states that for any type `α` that has a subset relation (`HasSubset α`), a strict subset relation (`HasSSubset α`), a non-strict strict order relation (`IsNonstrictStrictOrder α`), and an antisymmetric subset relation (`IsAntisymm α`), if `a` is a subset of `b`, then `a` is either a strict subset of `b` or `a` is equal to `b`. In other words, this theorem is asserting that a set `a` is strictly contained in another set `b`, or both sets are identical when `a` is a subset of `b`.
More concisely: If `α` is a type with a subset relation, strict subset relation, non-strict strict order relation, and antisymmetric subset relation, then for any sets `a` and `b` with `a ⊆ b`, we have `a ⊊ b` or `a = b`.
|
IsWellFounded.wf
theorem IsWellFounded.wf : ∀ {α : Type u} {r : α → α → Prop} [self : IsWellFounded α r], WellFounded r
This theorem states that for any type `α` and any binary relation `r` on `α`, if the relation is well-founded (as defined by the condition `IsWellFounded α r`), then `r` is a well-founded relation. In the context of set theory, a relation `r` on a set `α` is well-founded if every non-empty subset of `α` has a minimal element with respect to `r`. This property is fundamental in the theory of ordinals and in many parts of theoretical computer science.
More concisely: If `α` is a type and `r` is a binary relation on `α` such that `IsWellFounded α r` holds, then `r` is a well-founded relation.
|
WellFoundedLT.apply
theorem WellFoundedLT.apply :
∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α] (a : α), Acc (fun x x_1 => x < x_1) a
This theorem states that for any type `α` that has a less-than (`<`) relation and for which this less-than relation is well-founded, all elements `a` of this type are accessible. In the context of well-founded relations, an element is said to be accessible if there is no infinite descending chain starting from that element. This means there is no infinite sequence `a_1, a_2, a_3, ...` such that `a_{i+1} < a_i` for all `i`.
More concisely: For any type equipped with a well-founded order relation, every element is accessible.
|
IsAsymm.isIrrefl
theorem IsAsymm.isIrrefl : ∀ {α : Type u} {r : α → α → Prop} [inst : IsAsymm α r], IsIrrefl α r
This theorem states that, for any type `α` and a relation `r` over `α`, if `r` is asymmetric, then `r` is also irreflexive. In more mathematical terms, if for all `a` and `b` of type `α`, `r(a, b)` implies not `r(b, a)`, then for all `a` of type `α`, not `r(a, a)` holds. In simpler terms, if a relation doesn't allow both `r(a, b)` and `r(b, a)` to be true for any distinct elements `a` and `b`, then it also doesn't allow `r(a, a)` to be true for any element `a`.
More concisely: If a relation `r` over type `α` is asymmetric (i.e., `r(a, b)` implies `not r(b, a)` for all `a` and `b`), then it is irreflexive (i.e., `not r(a, a)` for all `a` in `α`).
|
antisymm_of'
theorem antisymm_of' : ∀ {α : Type u} (r : α → α → Prop) [inst : IsAntisymm α r] {a b : α}, r a b → r b a → b = a := by
sorry
This theorem states that for any type `α` and a binary relation `r` on `α`, if `r` is antisymmetric (i.e., if `r a b` and `r b a` are both true, then `a` must be equal to `b`), then for any two elements `a` and `b` of `α`, if `r a b` and `r b a` are both true, it follows that `b` is equal to `a`. This is a version of the `antisymm'` lemma where the relation `r` needs to be explicitly provided.
More concisely: If a binary relation `r` on a type `α` is antisymmetric, then for all `a` and `b` in `α`, if `r a b` and `r b a` hold, then `a` is equal to `b`.
|
ssubset_iff_subset_ne
theorem ssubset_iff_subset_ne :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊂ b ↔ a ⊆ b ∧ a ≠ b
This theorem states that for any type `α` that has subset (`HasSubset`) and strict subset (`HasSSubset`) operations, and for any elements `a` and `b` of type `α`, `a` is a strict subset of `b` if and only if `a` is a subset of `b` and `a` is not equal to `b`. This is under the conditions where the subset operation forms a non-strict strict order (`IsNonstrictStrictOrder`) over `α` and the subset operation is anti-symmetric (`IsAntisymm`).
More concisely: For any type `α` with `HasSubset` and `HasSSubset` operations, `a ⊆ b` and `a ≠ b` if and only if `a` is a strict subset of `b`, assuming the subset operation is a non-strict strict order and anti-symmetric.
|
Eq.trans_subset
theorem Eq.trans_subset : ∀ {α : Type u} [inst : HasSubset α] {a b c : α}, a = b → b ⊆ c → a ⊆ c
This theorem, "Eq.trans_subset," states a fundamental principle of set theory for any type `α` that has a subset. Specifically, it asserts that if we have three elements `a`, `b`, and `c` of type `α`, and if `a` is equal to `b` and `b` is a subset of `c`, then `a` is also a subset of `c`. This theorem is essentially an alias of `subset_of_eq_of_subset`.
More concisely: If `a` equals `b` and `b` is a subset of `c`, then `a` is a subset of `c`.
|
WellFoundedGT.fix_eq
theorem WellFoundedGT.fix_eq :
∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedGT α] {C : α → Sort u_1}
(F : (x : α) → ((y : α) → x < y → C y) → C x) (x : α),
WellFoundedGT.fix F x = F x fun y x => WellFoundedGT.fix F y
The theorem `WellFoundedGT.fix_eq` states that for any type `α` with a defined "less than" relation and a well-founded "greater than" relation, and any function `F` that maps an element `x` of type `α` and a function (that takes an element `y` of type `α` and a proof that `x` is less than `y` to give an element of type `C y`) to an element of type `C x`, the result of applying the function `WellFoundedGT.fix` to `F` and any element `x` of type `α` is the same as applying `F` to `x` and a function that takes `y` and a proof that `x` is less than `y` to `WellFoundedGT.fix F y`. In simpler terms, this theorem guarantees that the value produced by `WellFoundedGT.fix` is constructed from successive applications of the function `F` as specified.
More concisely: For any type `α` with well-founded order relations "<" and ">", and any function `F : α × (α × proof that x < y) → C`, the function `WellFoundedGT.fix F` applied to an element `x` of `α` is equivalent to applying `F` to `x` and a proof that `x` is less than any `y` and then recursively applying the result to `y` and the proof `x < y`.
|
HasSubset.Subset.antisymm'
theorem HasSubset.Subset.antisymm' :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → b ⊆ a → b = a
This theorem, named `HasSubset.Subset.antisymm'`, states that given any type `α` that has a subset relation (`HasSubset α`), and any two objects `a` and `b` of that type, if the subset relation is antisymmetric (`IsAntisymm α fun x x_1 => x ⊆ x_1`), then if `a` is a subset of `b` and `b` is a subset of `a`, it must be the case that `a` and `b` are equal. This is an alias of the `superset_antisymm` theorem. This theorem captures the antisymmetry property of the subset relation, a fundamental property in set theory.
More concisely: If `α` is a type with a subset relation and `IsAntisymm` holds for the subset relation on `α`, then for all `a` and `b` in `α`, `a ⊆ b` and `b ⊆ a` imply `a = b`.
|
WellFoundedGT.induction
theorem WellFoundedGT.induction :
∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedGT α] {C : α → Prop} (a : α),
(∀ (x : α), (∀ (y : α), x < y → C y) → C x) → C a
This theorem, `WellFoundedGT.induction`, is a statement about inductive reasoning on a well-founded `>` relation. Specifically, for any type `α` with a less than (`<`) operation and a well-founded `>` relation, if we have a property `C` that applies to elements of `α`, and for any `x` of type `α`, `C` holds for `x` whenever `C` holds for all `y` greater than `x`, then `C` holds for any element `a` of type `α`. This is essentially a form of mathematical induction tailored for well-founded relations.
More concisely: If `<` is a strict total order on `α` and `>` is a well-founded relation on `α`, then for any property `C` that is closed under the `>` relation, if `C` holds for the minimal elements and for all `x`, `C(x)` implies `C(y)` for all `y > x`, then `C` holds for every element of `α`.
|
comm
theorem comm : ∀ {α : Type u} {r : α → α → Prop} [inst : IsSymm α r] {a b : α}, r a b ↔ r b a
This theorem, referred to as 'comm', states that for any type `α` and any relation `r` on `α`, if the relation `r` is symmetric, then for any two elements `a` and `b` of type `α`, `r a b` will be equivalent to `r b a`. In simpler terms, it's saying that if `r` is a symmetric relation, then the order of the elements in the relation doesn't matter; if `a` is related to `b` then `b` is also related to `a`.
More concisely: If `r` is a symmetric relation on type `α`, then `r a b ↔ r b a` for all `a` and `b` of type `α`.
|
HasSubset.Subset.not_ssubset
theorem HasSubset.Subset.not_ssubset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}, a ⊆ b → ¬b ⊂ a
This theorem, `HasSubset.Subset.not_ssubset`, states that for any type `α` which has a subset and strict subset operation, and where these operations form a non-strict strict order, if `a` is a subset of `b`, then `b` cannot be a strict subset of `a`. In terms of set theory, if a set `a` is included in or equal to another set `b`, then we cannot have `b` strictly included in `a` (meaning `b` is a subset of `a` but not equal to `a`).
More concisely: If `a` is a subset of `b`, then `b` cannot be a strict subset of `a`.
|
antisymm_of
theorem antisymm_of : ∀ {α : Type u} (r : α → α → Prop) [inst : IsAntisymm α r] {a b : α}, r a b → r b a → a = b := by
sorry
This theorem, `antisymm_of`, states that for any type `α` and any relation `r` on `α`, if `α` is antisymmetric under `r`, then for any two elements `a` and `b` of `α`, if `a` is related to `b` and `b` is related to `a`, then `a` must be equal to `b`. This is an explicit version of the antisymmetry property, which is not directly stated in the core Lean libraries. In terms of mathematical notation, if `r` is an antisymmetric relation on a set, if `r(a, b)` and `r(b, a)` for some `a` and `b` in the set, then `a = b`.
More concisely: If `α` is a type with an antisymmetric relation `r`, then for all `a` and `b` in `α`, if `r(a, b)` and `r(b, a)` hold, then `a = b`.
|
HasSSubset.SSubset.false
theorem HasSSubset.SSubset.false :
∀ {α : Type u} [inst : HasSSubset α] [inst_1 : IsIrrefl α fun x x_1 => x ⊂ x_1] {a : α}, ¬a ⊂ a
This theorem, an alias of `ssubset_irrfl`, states that for any type `α` that has a "strict subset" operation (`HasSSubset α`), and where this "strict subset" relation is irreflexive (`IsIrrefl α fun x x_1 => x ⊂ x_1`), it is not the case that `a` is a strict subset of `a` for any `a` of type `α`. In other words, no element is a strict subset of itself.
More concisely: For any type `α` with an irreflexive strict subset relation `x ⊂ x_1`, there is no element `a` such that `a` is a strict subset of itself.
|
transitive_of_trans
theorem transitive_of_trans : ∀ {α : Type u} (r : α → α → Prop) [inst : IsTrans α r], Transitive r
This theorem states that for any type `α` and for any relation `r` on `α`, if `r` is a transitive relation (i.e., `r` fulfills the condition that for any three elements `x`, `y`, and `z` of `α`, if `x` is related to `y` by `r` and `y` is related to `z` by `r`, then `x` is also related to `z` by `r`), then `r` satisfies the property of being `Transitive`. In other words, if `r` is transitive, then `r` fulfills the property that for all `x`, `y`, and `z`, if `r x y` and `r y z`, then `r x z`.
More concisely: If `r` is a transitive relation on type `α`, then for all `x`, `y`, and `z` in `α`, `x` related to `y` by `r` and `y` related to `z` by `r` implies `x` related to `z` by `r`.
|
wellFounded_lt
theorem wellFounded_lt : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α], WellFounded fun x x_1 => x < x_1 := by
sorry
The theorem `wellFounded_lt` states that for any type `α` with a less-than (`<`) relation and for which the relation is well-founded (according to the `WellFoundedLT` definition), the less-than relation is well-founded. In other words, if we have a type `α` where the `<` relation is well-founded (meaning there are no infinite decreasing sequences), then the `<` relation itself is well-founded for any two elements of this type.
More concisely: If type `α` is equipped with a well-founded less-than relation `<`, then `<` is a well-founded relation on `α`.
|
IsTotal.swap
theorem IsTotal.swap : ∀ {α : Type u} (r : α → α → Prop) [inst : IsTotal α r], IsTotal α (Function.swap r)
The theorem `IsTotal.swap` states that for any type `α` and a relation `r` on `α` which is total, the swapped version of relation `r` is also total. Here, a relation is total if for any two elements `a` and `b` in `α`, either `r a b` or `r b a` holds. The swap operation on a relation is defined as the relation with its arguments switched, i.e., `r a b` becomes `r b a`.
More concisely: If `r` is a total relation on type `α`, then the swapped relation `r.symm` is also total.
|
eq_or_ssubset_of_subset
theorem eq_or_ssubset_of_subset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → a = b ∨ a ⊂ b
This theorem states that for any type `α` with a subset operation and a proper subset operation, which together form a nonstrict-strict order, and for any two elements `a` and `b` of that type, if the subset operation is also antisymmetric, then if `a` is a subset of `b`, it must be the case that `a` is equal to `b` or `a` is a proper subset of `b`.
More concisely: If `α` is a type with a subset operation, proper subset operation, and antisymmetric subset relation, then for all `a` and `b` in `α`, if `a` is a subset of `b`, then `a` is equal to `b` or `a` is a proper subset of `b`.
|
Set.not_bounded_iff
theorem Set.not_bounded_iff : ∀ {α : Type u} {r : α → α → Prop} (s : Set α), ¬Set.Bounded r s ↔ Set.Unbounded r s := by
sorry
This theorem states that for any given type `α` and a relation `r` on `α`, a set `s` of type `α` is not bounded under relation `r` if and only if it is unbounded under the same relation. In other words, a 'bounded' set has an element such that every element in the set is related to it through `r`, and an 'unbounded' set has the property that for every element of type `α`, there exists an element in the set that does not have this relation with the element of type `α`. The theorem asserts the equivalence of the negation of the former condition and the latter condition.
More concisely: A set is unbounded under a relation if and only if it is not bounded and there exists no upper bound in the set with respect to that relation.
|
subset_refl
theorem subset_refl : ∀ {α : Type u} [inst : HasSubset α] [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1] (a : α), a ⊆ a := by
sorry
This theorem, named `subset_refl`, states that for any type `α` that has a subset operation and is reflexive with respect to subset operation, any element `a` of type `α` is a subset of itself. In mathematical terms, it expresses the reflexivity of set inclusion: for any set `a`, `a` is included in `a`.
More concisely: For any type `α` with a reflexive subset relation, every element `a` in `α` is a subset of `{a}`.
|
of_eq
theorem of_eq : ∀ {α : Type u} {r : α → α → Prop} [inst : IsRefl α r] {a b : α}, a = b → r a b
This theorem states that for any type `α` and any binary relation `r` on `α`, given also that `r` is reflexive, if `a` and `b` are equal elements of type `α`, then `r a b` holds true. In other words, if `a` and `b` are the same element, then the reflexive relation `r` is fulfilled between `a` and `b`.
More concisely: If `r` is a reflexive binary relation on type `α`, then `r a a` holds for all `a` in `α`.
|
IsWellFounded.fix_eq
theorem IsWellFounded.fix_eq :
∀ {α : Type u} (r : α → α → Prop) [inst : IsWellFounded α r] {C : α → Sort u_1}
(F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α),
IsWellFounded.fix r F x = F x fun y x => IsWellFounded.fix r F y
The theorem `IsWellFounded.fix_eq` states that for any well-founded relation `r` on a type `α`, and for any function `F` that produces a value of some type `C` from an element of `α` and a function from `α` to `C`, the value produced by the `IsWellFounded.fix` function on `r` and `F` at any `x` in `α` is the same as the value produced by `F` at `x` with the function that maps any `y` in `α` to the value produced by `IsWellFounded.fix` on `r` and `F` at `y`. This essentially says that the `IsWellFounded.fix` function is defined recursively following the specification provided by the function `F`.
More concisely: For any well-founded relation `r` on type `α` and function `F` from `α × (α → C)` to `C`, `IsWellFounded.fix r F x = F x (λ y, IsWellFounded.fix r F y)`.
|
Ne.ssubset_of_subset
theorem Ne.ssubset_of_subset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}
[inst_3 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ≠ b → a ⊆ b → a ⊂ b
The theorem `Ne.ssubset_of_subset` states that for any two elements `a` and `b` of a type `α` that has both subset (`⊆`) and strict subset (`⊂`) relations, and these relations form a nonstrict-strict order, if `a` is not equal to `b` and `a` is a subset of `b`, then `a` is a strict subset of `b`. This theorem relies on the antisymmetry of the subset relation, which ensures that if both `a` is a subset of `b` and `b` is a subset of `a`, then `a` is equal to `b`.
More concisely: If `a` is a proper subset of `b` (i.e., `a ⊆ b` and `a ≠ b`) in a type `α` with a strict subset relation, then `a` is a strict subset of `b` (`a ⊂ b`).
|
HasSubset.Subset.antisymm
theorem HasSubset.Subset.antisymm :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsAntisymm α fun x x_1 => x ⊆ x_1], a ⊆ b → b ⊆ a → a = b
This theorem, which serves as an alias of `subset_antisymm`, states that for any type `α` that has a subset operation and an antisymmetry property with respect to this operation, if `a` is a subset of `b` and `b` is a subset of `a`, then `a` is equal to `b`. This theorem encapsulates the antisymmetry property of subsets: in the context of set theory, if two sets each include all elements of the other, they must be the same set.
More concisely: If `a` is a subset of `b` and `b` is a subset of `a`, then `a` equals `b`.
|
Eq.superset
theorem Eq.superset :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1], a = b → b ⊆ a
This theorem, referred to as `Eq.superset`, states that for any type `α` that has a subset operation, and for any two elements `a` and `b` of this type, if `a` equals `b`, then `b` is a subset of `a`. This holds under the condition that the subset relationship is reflexive on `α`, meaning any element of `α` is a subset of itself.
More concisely: If `α` is a type with a reflexive subset relation, then for all `a` and `b` in `α`, `a = b` implies `b ⊆ a`.
|
right_iff_left_not_left_of
theorem right_iff_left_not_left_of :
∀ {α : Type u} (r s : α → α → Prop) [inst : IsNonstrictStrictOrder α r s] {a b : α}, s a b ↔ r a b ∧ ¬r b a := by
sorry
This theorem states that for any type `α` and for any two relation functions `r` and `s` on `α`, given that `r` and `s` form a nonstrict strict order, the relation `s a b` holds if and only if both `r a b` holds and `r b a` does not hold, where `a` and `b` are elements of `α`. In layman's terms, this theorem describes a sort of "one-way" relationship between `a` and `b` under certain conditions.
More concisely: For any type `α` and relation functions `r` and `s` forming a non-strict strict order on `α`, `s(a, b)` holds if and only if `r(a, b)` holds and `r(b, a)` does not hold.
|
comm_of
theorem comm_of : ∀ {α : Type u} (r : α → α → Prop) [inst : IsSymm α r] {a b : α}, r a b ↔ r b a
This theorem states that for any type `α` and a binary relation `r` on `α`, if `r` is symmetric, then the relation holds between `a` and `b` if and only if it holds between `b` and `a`. This is essentially a version of the commutative property, where the relation `r` is made explicit. The theorem fills in a gap in Lean's core library under `Init.Algebra.Classes`, where a similar theorem may be missing.
More concisely: For any type `α` and symmetric binary relation `r` on `α`, `a` is related to `b` if and only if `b` is related to `a` (i.e., `r` is reflexive, symmetric, and transitive implies `a r b <=> b r a`).
|
ssubset_iff_subset_not_subset
theorem ssubset_iff_subset_not_subset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α},
a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a
The theorem `ssubset_iff_subset_not_subset` states that for any types `α`, given the type has the subset relationship (⊆), and the strict subset relationship (⊂), and the order of these relationships is nonstrict-strict (a strict subset is indeed a subset but not the other way around), then an element `a` is strictly subset of another element `b` if and only if `a` is a subset of `b` and `b` is not a subset of `a`. In simpler terms, `a` is strictly contained in `b` when `a` is contained in `b` and there is at least one element in `b` that is not in `a`.
More concisely: For types with the subset and strict subset relations (⊆ and ⊂, respectively), with the order being non-strict-strict, the strict subset relationship holds if and only if one set is a proper subset of the other, i.e., a set is strictly contained in another if and only if it is a subset but not vice versa and there exists an element in the larger set not in the smaller set.
|
HasSSubset.SSubset.ne'
theorem HasSSubset.SSubset.ne' :
∀ {α : Type u} [inst : HasSSubset α] [inst_1 : IsIrrefl α fun x x_1 => x ⊂ x_1] {a b : α}, a ⊂ b → b ≠ a
This theorem, which is an alias of `ne_of_ssuperset`, states that for any type `α` that has a strict subset operation and an irreflexive relation for this operation, if `a` is a strict subset of `b`, then `b` is not equal to `a`. In other words, if a set `a` is strictly contained within a set `b` (meaning that `b` contains at least one element that `a` does not), then `b` cannot be equal to `a`.
More concisely: For any type `α` with strict subset `⊆` and irreflexive relation `∉`, if `a ⊆ b` then `b ≠ a`.
|
HasSSubset.SSubset.subset
theorem HasSSubset.SSubset.subset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}, a ⊂ b → a ⊆ b
This is a theorem named `HasSSubset.SSubset.subset` in Lean 4 which states that for any type `α` with defined subset and strict subset operations, and for which these operations form a nonstrict strict order, if an element `a` is a strict subset of an element `b` (denoted `a ⊂ b`), then `a` is also a subset of `b` (denoted `a ⊆ b`). This theorem essentially captures the intuitive notion that if `a` is strictly contained in `b`, then `a` is certainly contained in `b`, whether or not `a` equals `b`.
More concisely: If `a` is a strict subset of `b` (`a ⊂ b`), then `a` is a subset of `b` (`a ⊆ b`).
|
WellFoundedLT.fix_eq
theorem WellFoundedLT.fix_eq :
∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α] {C : α → Sort u_1}
(F : (x : α) → ((y : α) → y < x → C y) → C x) (x : α),
WellFoundedLT.fix F x = F x fun y x => WellFoundedLT.fix F y
The `WellFoundedLT.fix_eq` theorem is a way of asserting that the values derived from the `WellFoundedLT.fix` operation are constructed from previous values according to a specified pattern. It is applicable to a well-founded relational structure (`WellFoundedLT`) over some type `α` with an order relation `<`. The theorem states that for any function `F` which generates a value `C x` for an element `x` of type `α` based on the values `C y` for all `y` that are less than `x`, and for any such `x`, the value produced by the `WellFoundedLT.fix` operation on `F` and `x` is identical to the value produced by applying `F` to `x` and to the function that, for any `y` less than `x`, gives the `WellFoundedLT.fix` operation on `F` and `y`. In other words, `WellFoundedLT.fix` builds its results in the way that `F` says to build them.
More concisely: Given a well-founded relation `<` on type `α` and a function `F : α → α` such that `x = WellFoundedLT.fix F x <-∏ y < x (WellFoundedLT.fix F y),` then `x = WellFoundedLT.fix F (F x)`.
|
subset_rfl
theorem subset_rfl : ∀ {α : Type u} [inst : HasSubset α] {a : α} [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1], a ⊆ a := by
sorry
This theorem, `subset_rfl`, states that for any type `α` that has a notion of subset (`HasSubset α`), any element `a` of this type is a subset of itself. This property, derived from the reflexivity axiom (`IsRefl α`), is one of the fundamental properties of set theory.
More concisely: For any type `α` with subset structure, every element `a` in `α` is a subset of `{a}`.
|
subset_of_eq
theorem subset_of_eq :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1], a = b → a ⊆ b
This theorem states that for any type `α` that has a subset operation, given any two elements `a` and `b` of this type, and assuming that the subset operation is reflexive, if `a` equals `b` then `a` is a subset of `b`. In other words, equality implies the subset relation for any two objects in a type where the subset operation is defined and is reflexive.
More concisely: If `α` is a type with reflexive subset relation, then for all `a` and `b` in `α`, `a = b` implies `a ⊆ b`.
|
WellFoundedLT.induction
theorem WellFoundedLT.induction :
∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α] {C : α → Prop} (a : α),
(∀ (x : α), (∀ y < x, C y) → C x) → C a
This theorem, named `WellFoundedLT.induction`, is a form of mathematical induction for a well-founded less-than relation. For any type `α` equipped with a less-than relation and assumed to be well-founded, if we have a property `C` and an element `a` of type `α`, the theorem states that if for all `x` of type `α`, the implication "if `C` holds for all `y` less than `x`, then `C` holds for `x`" is true, then `C` must also hold for `a`. Thus, it provides a way to inductively prove that a property holds for all elements of a type, under the assumption that the less-than relation on the type is well-founded.
More concisely: If `α` is a well-founded type with a less-than relation, and for all `x` in `α`, if `C` holds for all `y` less than `x`, then `C` holds for `x`, then `C` holds for every element `a` in `α`.
|
Eq.subset'
theorem Eq.subset' :
∀ {α : Type u} [inst : HasSubset α] {a b : α} [inst_1 : IsRefl α fun x x_1 => x ⊆ x_1], a = b → a ⊆ b
This theorem, which is an alias of `subset_of_eq`, states that for any type `α` that has a subset operation and a reflexivity relation defined on it, if `a` and `b` are elements of `α` and `a` is equal to `b`, then `a` is a subset of `b`.
More concisely: For all types `α` with defined subset and equality relations, if `a` and `b` are elements of `α` with `a = b`, then `a ⊆ b`.
|
HasSSubset.SSubset.not_subset
theorem HasSSubset.SSubset.not_subset :
∀ {α : Type u} [inst : HasSubset α] [inst_1 : HasSSubset α]
[inst_2 : IsNonstrictStrictOrder α (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1] {a b : α}, a ⊂ b → ¬b ⊆ a
This theorem, which is an alias for `not_subset_of_ssubset`, states for any type `α` equipped with subset and strict subset relations, and where these relations form a nonstrict strict order, if `a` is a strict subset of `b` (`a ⊂ b`), then `b` is not a subset of `a` (`¬b ⊆ a`). In other words, if `a` is strictly contained in `b`, then `b` cannot be fully contained in `a`. This aligns with the intuitive idea of strict subset where `a` is a subset of `b` but `a` is not equal to `b`.
More concisely: If `a` strictly contains `b`, then `b` is not a subset of `a`. In mathematical notation, `a ⊂ b` implies `¬b ⊆ a`.
|
HasSSubset.SSubset.trans
theorem HasSSubset.SSubset.trans :
∀ {α : Type u} [inst : HasSSubset α] [inst_1 : IsTrans α fun x x_1 => x ⊂ x_1] {a b c : α}, a ⊂ b → b ⊂ c → a ⊂ c
This theorem, named `HasSSubset.SSubset.trans`, states that for any type `α` that has a strict subset operation (denoted by `⊂`), and where this operation is transitive, if `a` is a strict subset of `b`, and `b` is a strict subset of `c`, then `a` is a strict subset of `c`. This is essentially the transitivity property for strict subset relation.
More concisely: If `α` has a transitive strict subset relation `⊂`, then `a ⊂ b` and `b ⊂ c` imply `a ⊂ c`.
|