ZFSet.image.mk
theorem ZFSet.image.mk :
∀ (f : ZFSet → ZFSet) [H : PSet.Definable 1 f] (x : ZFSet) {y : ZFSet}, y ∈ x → f y ∈ ZFSet.image f x
The theorem `ZFSet.image.mk` states that for any function `f` from ZFSet to ZFSet that is definable in the sense of PSet, and for any sets `x` and `y` in the ZFSet universe, if `y` is an element of `x`, then the image of `y` under the function `f` is an element of the image set of `x` under `f`. In other words, if $y \in x$ then $f(y) \in \text{image of } f \text{ on } x$. This is a formalization of the familiar property of image of a function in set theory.
More concisely: For any function `f` from a set `x` to a set `y` in the ZFSet universe that preserves elements (i.e., `y ∋ f(y)` for all `y ∈ x`), the image of an element `y` under `f` belongs to the image set of `x` under `f`.
|
ZFSet.pair_injective
theorem ZFSet.pair_injective : Function.Injective2 ZFSet.pair
The theorem `ZFSet.pair_injective` states that the function `ZFSet.pair`, which creates a Kuratowski ordered pair from two elements of the type `ZFSet`, is injective in both of its arguments. In other words, given any four elements `a₁`, `a₂`, `b₁`, `b₂` of `ZFSet`, if `ZFSet.pair a₁ b₁` equals `ZFSet.pair a₂ b₂`, then `a₁` must be equal to `a₂` and `b₁` must be equal to `b₂`. This maps mathematically to the injective property of the function `α × β → γ` in the domain of ZFSet, where different ordered pairs have distinct results.
More concisely: If `a₁`, `a₂`, `b₁`, `b₂` are elements of `ZFSet` such that `ZFSet.pair a₁ b₁` equals `ZFSet.pair a₂ b₂`, then `a₁` equals `a₂` and `b₁` equals `b₂`.
|
Class.ext
theorem Class.ext : ∀ {x y : Class}, (∀ (z : ZFSet), x z ↔ y z) → x = y
The theorem `Class.ext` states that for any two classes `x` and `y`, if for every set `z` in the Zermelo-Fraenkel universe of sets (`ZFSet`), `z` belongs to `x` if and only if `z` belongs to `y`, then `x` and `y` are equal. In other words, it states that two classes are equal if they contain exactly the same sets.
More concisely: If two classes `x` and `y` have the same elements in the Zermelo-Fraenkel universe of sets (`ZFSet`), then `x` is equal to `y`.
|
Mathlib.SetTheory.ZFC.Basic._auxLemma.15
theorem Mathlib.SetTheory.ZFC.Basic._auxLemma.15 : ∀ (x : ZFSet), (x ∈ ∅) = False
This theorem states that for all x, where x is of type ZFSet (the ZFC universe of sets), x is not a member of the empty set. In other words, it asserts that the empty set does not contain any elements.
More concisely: The theorem asserts that the empty set is empty and contains no elements, that is, ∀x, x ∉ ∅.
|
ZFSet.mem_insert_iff
theorem ZFSet.mem_insert_iff : ∀ {x y z : ZFSet}, x ∈ insert y z ↔ x = y ∨ x ∈ z
This theorem states that for any three elements `x`, `y`, and `z` from the ZFC universe of sets, `x` is an element of the set formed by inserting `y` into `z` if and only if `x` is equal to `y` or `x` is an element of `z`. This is a statement of the basic property of set formation in Zermelo-Fraenkel set theory.
More concisely: For any sets x, y, and z, x is an element of {y | z} if and only if x is equal to y or x is an element of z. (This is the definition of set formation in Zermelo-Fraenkel set theory.)
|
ZFSet.mem_sUnion
theorem ZFSet.mem_sUnion : ∀ {x y : ZFSet}, y ∈ x.sUnion ↔ ∃ z ∈ x, y ∈ z
The theorem `ZFSet.mem_sUnion` states that for all sets `x` and `y` in the ZFC universe of sets, `y` is an element of the union over `x` if and only if there exists a set `z` such that `z` is an element of `x` and `y` is an element of `z`. This theorem asserts the membership criterion for the union of a collection of sets in the ZFC set theory.
More concisely: For all sets x and y in the ZFC universe, y is an element of the union of x if and only if there exists a set z in x such that y is an element of z.
|
ZFSet.mem_sUnion_of_mem
theorem ZFSet.mem_sUnion_of_mem : ∀ {x y z : ZFSet}, y ∈ z → z ∈ x → y ∈ x.sUnion
This theorem states that for any three sets `x`, `y`, and `z` in the ZFSet (which is the Zermelo-Fraenkel set theory universe), if `y` is an element of `z` and `z` is an element of `x`, then `y` is an element of the union over all elements of `x` (written as ⋃₀ `x` in Lean 4). This captures the intuitive idea from set theory that if a set is nested within another set which is in turn nested within a larger set, then the innermost set is also a part of the largest set when we take the union of all its elements.
More concisely: If `y` is an element of `z` and `z` is an element of `x`, then `y` is an element of the union of `x`.
|
ZFSet.mem_powerset
theorem ZFSet.mem_powerset : ∀ {x y : ZFSet}, y ∈ x.powerset ↔ y ⊆ x
This theorem, `ZFSet.mem_powerset`, states that for any two ZF sets `x` and `y`, `y` is an element of the powerset of `x` if and only if `y` is a subset of `x`. In other words, it sets up an equivalence between a ZF set `y` being in the powerset of `x` and `y` being a subset of `x`, which is a fundamental property of powersets in set theory.
More concisely: For any ZF sets `x` and `y`, `y` is an element of the powerset of `x` if and only if `y` is a subset of `x`.
|
ZFSet.Hereditarily.def
theorem ZFSet.Hereditarily.def :
∀ {p : ZFSet → Prop} {x : ZFSet}, ZFSet.Hereditarily p x → p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y
This theorem, referred to as an alias of the forward direction of `ZFSet.hereditarily_iff`, states that for every predicate `p` on ZFSet and every set `x` in ZFSet, if `x` is hereditarily `p` (i.e., both `x` and all its elements satisfy `p`), then `x` satisfies `p` and for every element `y` in `x`, `y` is also hereditarily `p`. In other words, a set `x` is hereditarily `p` only if it satisfies `p` and every element within `x` is likewise hereditarily `p`.
More concisely: A set is hereditarily p if and only if it satisfies p and every element is hereditarily p.
|
PSet.Equiv.refl
theorem PSet.Equiv.refl : ∀ (x : PSet), x.Equiv x
The theorem `PSet.Equiv.refl` states that for any pre-set `x`, the pre-set `x` is extensionally equivalent to itself. In other words, every element of the pre-set `x` is extensionally equivalent to some element of the same pre-set `x` and vice-versa. This is a reflection of the reflexivity property in the context of extensional equivalence of pre-sets.
More concisely: Every pre-set is extensionally equivalent to itself.
|
PSet.mem_wf
theorem PSet.mem_wf : WellFounded fun x x_1 => x ∈ x_1
This theorem, `PSet.mem_wf`, states that the relation "is an element of" (`∈`) on the class of all Power Sets (`PSet`) is well-founded. In the context of set theory, a relation is said to be well-founded if there are no infinitely descending chains, which means that we cannot keep finding smaller and smaller elements indefinitely. In this case, we cannot find an infinite descending chain of sets within power sets.
More concisely: The relation "is an element of" on the class of all power sets is well-founded, meaning there are no infinite descending sets.
|
ZFSet.mem_sep
theorem ZFSet.mem_sep : ∀ {p : ZFSet → Prop} {x y : ZFSet}, y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y
The theorem `ZFSet.mem_sep` states that for any property `p` and any sets `x` and `y` in the Zermelo-Fraenkel set theory universe, `y` belongs to the set of elements in `x` that satisfy `p` if and only if `y` is an element of `x` and `y` satisfies the property `p`. In other words, it formalizes the notion of set membership for a subset defined by a property in ZF set theory. This theorem is essentially the mathematical version of the principle of restricted comprehension in set theory.
More concisely: For any set X and property p, y is in the subset of X satisfying p if and only if y is in X and has property p.
|
ZFSet.mem_image
theorem ZFSet.mem_image :
∀ {f : ZFSet → ZFSet} [H : PSet.Definable 1 f] {x y : ZFSet}, y ∈ ZFSet.image f x ↔ ∃ z ∈ x, f z = y
The theorem `ZFSet.mem_image` states that for any function `f` from Zermelo-Fraenkel sets (`ZFSet`) to `ZFSet` that is definable (meaning it corresponds to a formula in the language of set theory with one free variable), and for any Zermelo-Fraenkel sets `x` and `y`, `y` is an element of the image of `x` under `f` (denoted as `ZFSet.image f x`) if and only if there exists an element `z` in `x` such that `f z` equals `y`. In other words, this theorem asserts the basic property of images of functions in the context of Zermelo-Fraenkel set theory.
More concisely: For any definable function `f` from Zermelo-Fraenkel sets to Zermelo-Fraenkel sets and any sets `x` and `y`, `y` is an element of `f(x)` if and only if there exists an element `z` in `x` such that `f(z) = y`.
|
Mathlib.SetTheory.ZFC.Basic._auxLemma.25
theorem Mathlib.SetTheory.ZFC.Basic._auxLemma.25 : ∀ {x y : ZFSet}, (y ∈ x.sUnion) = ∃ z ∈ x, y ∈ z
This theorem from the Mathlib Set Theory ZFC library states that for any two sets `x` and `y` in the ZFC universe of sets, `y` is a member of the union over `x` if and only if there exists a subset `z` of `x` such that `y` is a member of `z`. In other words, a set `y` belongs to the union of a collection of sets `x` if `y` belongs to at least one set in that collection.
More concisely: For any sets `x` and `y`, `y` is in the union of `x` if and only if there exists a subset `z` of `x` such that `y` is in `z`.
|
Class.iota_ex
theorem Class.iota_ex : ∀ (A : Class), A.iota ∈ Class.univ
The theorem `Class.iota_ex` asserts that for every `Class` `A`, the `iota` definite descriptor of `A` is a member of the universal class. Unlike other set constructors, the `iota` definite descriptor always produces a set for any set input. However, this is not the case in a constructive manner, thus there is no associated function from `Class` to `Set`.
More concisely: The theorem `Class.iota_ex` states that for every type class `A`, the `iota` definite descriptor of `A` is an element of the universal set.
|
ZFSet.mem_wf
theorem ZFSet.mem_wf : WellFounded fun x x_1 => x ∈ x_1
This theorem, `ZFSet.mem_wf`, states that the membership relation "∈" on Zermelo-Fraenkel sets is well-founded. This means that there are no infinite descending chains of elements, i.e., there does not exist an infinite sequence {x1, x2, x3, ...} of sets such that x_{n+1} ∈ x_n for all natural numbers n. This property is essential in the set theory to avoid paradoxes such as Russell's paradox.
More concisely: The theorem `ZFSet.mem_wf` asserts that the membership relation on Zermelo-Fraenkel sets is well-founded, ensuring the absence of infinite descending chains.
|
Mathlib.SetTheory.ZFC.Basic._auxLemma.20
theorem Mathlib.SetTheory.ZFC.Basic._auxLemma.20 : ∀ {x y : ZFSet}, (x ∈ {y}) = (x = y)
This theorem, from the Mathlib library in set theory and specifically Zermelo-Fraenkel set theory, states that for any two sets `x` and `y` in the ZFC universe, `x` is an element of the singleton set `{y}` if and only if `x` is equal to `y`. In other words, a set `x` is in the set that contains only `y` exactly when `x` is `y`.
More concisely: For any sets `x` and `y` in the ZFC universe, `x` is an element of the singleton set `{y}` if and only if `x = y`.
|
Class.univ_not_mem_univ
theorem Class.univ_not_mem_univ : Class.univ ∉ Class.univ
The theorem `Class.univ_not_mem_univ` states that there is no universal set. More specifically, it asserts that the universal class, represented as `univ` (which should be interpreted as the class of all sets), does not contain itself. This means that the universal class is a proper class, meaning it does not belong to itself. This is an essential concept in set theory that helps to avoid paradoxes like the Russell's paradox.
More concisely: The universal class `univ` does not belong to itself in Lean 4 set theory.
|
ZFSet.inductionOn
theorem ZFSet.inductionOn : ∀ {p : ZFSet → Prop} (x : ZFSet), (∀ (x : ZFSet), (∀ y ∈ x, p y) → p x) → p x
This theorem deals with the principle of induction on the membership (`∈`) relation in the Zermelo-Fraenkel (ZF) universe of sets. It states that for any property `p` and any set `x` in the ZF universe, if we assume that the property `p` holds for every member `y` of `x`, then property `p` must also hold for `x` itself. This is an essential principle for proving properties of sets in the ZF universe, similar to structural induction in other mathematical contexts.
More concisely: If `p(x)` is a property and for all `y ∈ x`, `p(y)` holds, then `p(x)` also holds. (Principle of Induction on membership in ZF)
|
Class.eq_univ_of_powerset_subset
theorem Class.eq_univ_of_powerset_subset : ∀ {A : Class}, A.powerset ⊆ A → A = Class.univ
This theorem is an induction principle for sets. It states that for any class `A`, if every subset of `A` (also known as the powerset of `A`) is a member of `A` itself, then `A` must be the universal class. In simpler terms, if a class contains all of its own subsets, it is the class of all sets.
More concisely: If a set includes all its subsets, then it is the universal set.
|
PSet.Equiv.rfl
theorem PSet.Equiv.rfl : ∀ {x : PSet}, x.Equiv x
This theorem states that for any pre-set `x`, `x` is extensionally equivalent to itself. In mathematical terms, for any pre-set `x` (denoted as `PSet.mk α A`), for every element `a` in α, there exists an element `b` such that a is extensionally equivalent to `B b`, and vice versa. Essentially, this theorem is asserting the reflexivity of extensional equivalence on pre-sets.
More concisely: For any pre-set `x` (`PSet.mk α A`), every element `a` in `α` is extensionally equivalent to itself.
|
PSet.Equiv.euc
theorem PSet.Equiv.euc : ∀ {x : PSet} {y : PSet} {z : PSet}, x.Equiv y → z.Equiv y → x.Equiv z
The theorem `PSet.Equiv.euc` states that for any pre-sets `x`, `y`, and `z`, if `x` is extensionally equivalent to `y` and `z` is also extensionally equivalent to `y`, then `x` is extensionally equivalent to `z`. In other words, it establishes the Euclidean property for the extensional equivalence of pre-sets, which is a form of transitivity property through a common equivalent pre-set `y`.
More concisely: If pre-sets `x`, `y`, and `z` are pairwise extensionally equivalent, then `x` is extensionally equivalent to `z`.
|
ZFSet.mem_sInter
theorem ZFSet.mem_sInter : ∀ {x y : ZFSet}, x.Nonempty → (y ∈ x.sInter ↔ ∀ z ∈ x, y ∈ z)
This theorem states that for any two Zermelo-Fraenkel (ZF) sets, `x` and `y`, if `x` is nonempty, then `y` is an element of the intersection of all the sets in `x` if and only if `y` is an element of every set `z` that is an element of `x`. Here, `⋂₀ x` represents the intersection of all sets within `x`.
More concisely: For any nonempty set `x` in ZF, an element `y` belongs to the intersection of all sets in `x` if and only if it belongs to every set in `x`.
|
ZFSet.ext
theorem ZFSet.ext : ∀ {x y : ZFSet}, (∀ (z : ZFSet), z ∈ x ↔ z ∈ y) → x = y
This theorem, `ZFSet.ext`, states that for any two ZFSet types `x` and `y`, if for every ZFSet type `z`, `z` is an element of `x` if and only if `z` is an element of `y`, then `x` and `y` are equal. In other words, this is an extensionality theorem for the ZFSet type, asserting that two sets are identical if they have the same members. This concept is a fundamental axiom in many formulations of set theory.
More concisely: Two ZFSets `x` and `y` are equal if they have the same elements.
|
Class.coe_mem
theorem Class.coe_mem : ∀ {x : ZFSet} {A : Class}, ↑x ∈ A ↔ A x
The theorem `Class.coe_mem` states that for any set `x` from the ZFC universe of sets (`ZFSet`) and any `Class` `A`, the set `x` belongs to the class `A` if and only if the class `A` contains the set `x`. This theorem establishes the equivalence between the membership of a set in a class and the class containing the set.
More concisely: For any set `x` in the ZFC universe and class `A`, `x` belongs to `A` if and only if `A` contains `x`.
|
PSet.Mem.mk
theorem PSet.Mem.mk : ∀ {α : Type u} (A : α → PSet) (a : α), A a ∈ PSet.mk α A
This theorem, `PSet.Mem.mk`, asserts that, given any type `α`, any function `A` from `α` to `PSet` (the set of all sets), and any element `a` of `α`, `A a` is an element of the set `PSet.mk α A`. This essentially means that any application of the function `A` to an element of its domain `α` results in an element of the set defined by `α` and `A`.
More concisely: For any type `α` and function `A` from `α` to sets, `A a` is an element of the set `PSet.mk α A` for all `a` in `α`.
|
ZFSet.not_mem_empty
theorem ZFSet.not_mem_empty : ∀ (x : ZFSet), x ∉ ∅
This theorem states that for any element `x` of the ZFC universe of sets (`ZFSet`), `x` is not a member of the empty set (∅). This is in line with the standard set theory assertion that the empty set does not contain any elements.
More concisely: The theorem asserts that for all sets `x` in ZFC universe, `x ∉ ∅`.
|
ZFSet.mem_inter
theorem ZFSet.mem_inter : ∀ {x y z : ZFSet}, z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y
This theorem states that for any three sets `x`, `y`, and `z` in the ZFSet (the universe of Zermelo–Fraenkel set theory), `z` is a member of the intersection of `x` and `y` if and only if `z` is a member of `x` and `z` is a member of `y`. In other words, this theorem formalizes the basic set theory concept that an element belongs to the intersection of two sets precisely when it belongs to both sets.
More concisely: For any sets x, y in ZFSet, z belongs to the intersection of x and y if and only if z is an element of both x and y.
|
Mathlib.SetTheory.ZFC.Basic._auxLemma.19
theorem Mathlib.SetTheory.ZFC.Basic._auxLemma.19 : ∀ {x y z : ZFSet}, (x ∈ insert y z) = (x = y ∨ x ∈ z)
This theorem states that for any three sets `x`, `y`, and `z` in the Zermelo–Fraenkel set theory universe (`ZFSet`), `x` is an element of the set obtained by inserting `y` into `z` if and only if `x` is equal to `y` or `x` is an element of `z`. This mirrors the familiar property of sets in classical set theory.
More concisely: For any sets `x`, `y`, and `z` in `ZFSet`, `x ∈ {y | ∈ z} <--> x = y ∨ x ∈ z`.
|
PSet.equiv_iff
theorem PSet.equiv_iff :
∀ {x : PSet} {y : PSet},
x.Equiv y ↔
(∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)
The theorem `PSet.equiv_iff` states that for any two pre-sets `x` and `y`, they are extensionally equivalent (denoted by `PSet.Equiv x y`) if and only if the following two conditions are met: Firstly, for every element `i` in the underlying type of the pre-set `x` (denoted by `PSet.Type x`), there exists an element `j` such that the pre-set derived from `x` at `i` (denoted by `PSet.Func x i`) is extensionally equivalent to the pre-set derived from `y` at `j` (denoted by `PSet.Func y j`). Secondly, for every element `j` in the underlying type of the pre-set `y` (denoted by `PSet.Type y`), there exists an element `i` such that the pre-set derived from `x` at `i` is extensionally equivalent to the pre-set derived from `y` at `j`. This theorem essentially sets up a bijective relationship between the elements of the underlying types of two extensionally equivalent pre-sets.
More concisely: Two pre-sets are extensionally equivalent if and only if there exists a bijection between their underlying types such that the derived pre-sets at corresponding elements are extensionally equivalent.
|
Mathlib.SetTheory.ZFC.Basic._auxLemma.23
theorem Mathlib.SetTheory.ZFC.Basic._auxLemma.23 :
∀ {p : ZFSet → Prop} {x y : ZFSet}, (y ∈ ZFSet.sep p x) = (y ∈ x ∧ p y)
The theorem `_auxLemma.23` in the `Mathlib.SetTheory.ZFC.Basic` module states that for any predicate `p` and any Zermelo–Fraenkel set theory (ZFC) sets `x` and `y`, `y` is an element of the set of elements in `x` that satisfy `p` (represented by `ZFSet.sep p x`) if and only if `y` is an element of `x` and `y` satisfies `p`. In mathematical notation, this would be expressed as ∀p, x, y, (y ∈ {x ∈ a | p(x)}) ⇔ (y ∈ a ∧ p(y)).
More concisely: For any set `a` and predicate `p`, an element `y` is in the subset of `a` satisfying `p` if and only if it is in `a` and satisfies `p` itself.
|
ZFSet.eq_empty
theorem ZFSet.eq_empty : ∀ (x : ZFSet), x = ∅ ↔ ∀ (y : ZFSet), y ∉ x
This theorem states that for any set `x` in the ZFC universe of sets, `x` is equal to the empty set if and only if for all sets `y`, `y` is not an element of `x`. In other words, a set `x` is empty if it does not contain any other set.
More concisely: A set is empty if and only if it has no elements.
|
Class.coe_apply
theorem Class.coe_apply : ∀ {x y : ZFSet}, ↑y x ↔ x ∈ y
This theorem, named `Class.coe_apply`, states that for any two Zermelo-Fraenkel set theory (ZFC) sets `x` and `y`, the application of the coercion function `↑y` to `x` is equivalent to `x` being an element of `y`. The coercion function `↑y` transforms `y` from a ZFC set to a class. This theorem bridges the concept of set membership in the ZFC universe with the concept of function application in the class universe.
More concisely: For any sets `x` and `y` in ZFC, `x ∈ y` if and only if `↑y x = x`.
|
PSet.Equiv.symm
theorem PSet.Equiv.symm : ∀ {x : PSet} {y : PSet}, x.Equiv y → y.Equiv x
This theorem, `PSet.Equiv.symm`, states that the relation of extensional equivalence between two pre-sets is symmetric. In other words, for any pre-sets `x` and `y`, if `x` is extensionally equivalent to `y` (denoted as `PSet.Equiv x y`), then `y` is also extensionally equivalent to `x` (denoted as `PSet.Equiv y x`). The extensional equivalence between two pre-sets is defined as each element of the first pre-set being extensionally equivalent to some element of the second pre-set and vice versa.
More concisely: If pre-sets `x` and `y` are extensionally equivalent, then they are equal in the symmetric sense (i.e., `x = y`).
|
ZFSet.sound
theorem ZFSet.sound : ∀ {x y : PSet}, x.Equiv y → ZFSet.mk x = ZFSet.mk y
This theorem, `ZFSet.sound`, states that for any two pre-sets, `x` and `y`, if these two pre-sets are extensionally equivalent (as defined by `PSet.Equiv`, i.e., every element of the first pre-set is extensionally equivalent to some element of the second pre-set and vice versa), then the ZFC set representation (obtained via `ZFSet.mk`) of `x` and `y` are equal. In other words, it ensures the soundness of the function that constructs a ZFC set from a pre-set, in that extensionally equivalent pre-sets yield the same ZFC set.
More concisely: If two pre-sets are extensionally equivalent, then their corresponding ZFC sets are equal.
|
PSet.Equiv.trans
theorem PSet.Equiv.trans : ∀ {x : PSet} {y : PSet} {z : PSet}, x.Equiv y → y.Equiv z → x.Equiv z
This theorem establishes the transitivity property for the equivalence of pre-sets. In more detail, given any three pre-sets, `x`, `y`, and `z`, if `x` is equivalent to `y` and `y` is equivalent to `z`, then `x` is also equivalent to `z`. Here, the equivalence of two pre-sets is defined as each element of the first pre-set being extensionally equivalent to some element of the second pre-set and vice versa.
More concisely: If pre-sets `x` and `y` are equivalent, and `y` and `z` are equivalent, then `x` and `z` are equivalent. (Extensional equality preserves transitivity)
|
Mathlib.SetTheory.ZFC.Basic._auxLemma.9
theorem Mathlib.SetTheory.ZFC.Basic._auxLemma.9 : ∀ (a u : ZFSet), (a ∈ u.toSet) = (a ∈ u)
This theorem states that for all ZFSet (Zermelo–Fraenkel Set Theory) elements 'a' and 'u', 'a' is an element of the set represented by 'u' (obtained using `ZFSet.toSet` function) if and only if 'a' is an element of 'u' itself. In other words, the function `ZFSet.toSet` preserves the membership relation in the ZFSet universe.
More concisely: For all 'a' and 'u' in ZFSet, 'a' is an element of the set `ZFSet.toSet u` if and only if 'a' is an element of 'u'.
|
PSet.Equiv.eq
theorem PSet.Equiv.eq : ∀ {x y : PSet}, x.Equiv y ↔ x.toSet = y.toSet
This theorem states that two pre-sets (or classes of objects) are equivalent if and only if they have the exact same members. In other words, if we compare two pre-sets `x` and `y`, they are considered equivalent (`x.Equiv y`) if and only if transforming each pre-set to a set (`x.toSet` and `y.toSet`) yields the same set.
More concisely: Two pre-sets `x` and `y` are equivalent if and only if their sets of elements are equal: `x.Equiv y <-> x.toSet = y.toSet`.
|
PSet.Mem.congr_right
theorem PSet.Mem.congr_right : ∀ {x y : PSet}, x.Equiv y → ∀ {w : PSet}, w ∈ x ↔ w ∈ y
This theorem, `PSet.Mem.congr_right`, states that for any two pre-sets `x` and `y` that are extensionally equivalent, as defined by `PSet.Equiv x y`, any pre-set `w` is a member of `x` if and only if it is a member of `y`. In other words, if `x` and `y` are extensionally equivalent pre-sets, then their membership properties are congruent for any pre-set `w`.
More concisely: If two pre-sets `x` and `y` are extensionally equivalent, then for all pre-set `w`, `w ∈ x` if and only if `w ∈ y`.
|