Sublattice.coe_inj
theorem Sublattice.coe_inj : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α}, ↑L = ↑M ↔ L = M
This theorem, `Sublattice.coe_inj`, states that for any given type `α` that's a lattice, and for any two sublattices `L` and `M` of this lattice, the coercion of `L` to `α` being equal to the coercion of `M` to `α` is equivalent to `L` and `M` being equal. Coercion, denoted by `↑`, is a way to convert one type into another in Lean. Here, it's used to convert sublattices into their containing lattice. The theorem essentially says that if two sublattices are equal when viewed as sets in the larger lattice, then they are indeed equal as sublattices.
More concisely: For any lattice type `α` and sublattices `L` and `M` of `α`, `↑L = ↑M` if and only if `L = M`.
|
Sublattice.infClosed
theorem Sublattice.infClosed : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), InfClosed ↑L
This theorem states that for any type `α` that forms a lattice, given a sublattice `L` of `α`, `L` is "inf-closed". In mathematical terms, this means that for any two elements `a` and `b` in the sublattice `L`, their infimum (`a ⊓ b`) is also in `L`. This property is fundamental to the theory of lattices and sublattices.
More concisely: For any lattice `α` and sublattice `L` of `α`, the infimum of any two elements in `L` lies in `L`.
|
Sublattice.ext
theorem Sublattice.ext : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α}, (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M
This theorem states that for any type `α`, which is a lattice, two sublattices `L` and `M` are identical if and only if they contain exactly the same elements. This is a fundamental theorem in lattice theory and set theory alike. In other words, if any element `a` of type `α` is in sublattice `L` if and only if it is also in sublattice `M`, then `L` and `M` are in fact the same sublattice.
More concisely: For any lattice `α`, sublattices `L` and `M` are equal if and only if they have the same elements.
|
Sublattice.supClosed
theorem Sublattice.supClosed : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), SupClosed ↑L
The theorem `Sublattice.supClosed` states that for any type `α` that forms a lattice structure, every sublattice `L` of this lattice is supremum-closed, meaning that for all elements `a` and `b` in the sublattice `L`, their supremum `a ⊔ b` also belongs to `L`.
More concisely: For any lattice `α` and sublattice `L` of `α`, every supremum of elements in `L` lies in `L`.
|
Sublattice.gc_map_comap
theorem Sublattice.gc_map_comap :
∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
GaloisConnection (Sublattice.map f) (Sublattice.comap f)
This theorem states that for any two types `α` and `β` that are lattices and a given lattice homomorphism `f` from `α` to `β`, there exists a Galois connection between the mapping of a sublattice from `α` to `β` using `f` (denoted as `Sublattice.map f`) and the preimage of a sublattice from `β` to `α` along `f` (denoted as `Sublattice.comap f`). In simpler terms, this means that the mapping of a sublattice from `α` to `β` is less than or equal to a sublattice in `β` if and only if the original sublattice in `α` is less than or equal to the preimage of the sublattice in `β`. The existence of such a Galois connection illustrates a fundamental relationship between the structure of lattices and their sublattices under lattice homomorphisms.
More concisely: For any lattice homomorphism between lattices `α` and `β`, there exists a Galois connection between the mapping of sublattices using `f` and the preimage of sublattices along `f`.
|