Documentation

Mathlib.Order.CompleteLattice.SetLike

SetLike instance for elements of CompleteSublattice (Set X) #

This file provides lemmas for the SetLike instance for elements of CompleteSublattice (Set X)

source
theorem Sublattice.ext_mem {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L} (h : ∀ (x : X), x ∈ S ↔ x ∈ T) :
S = T
source
theorem Sublattice.mem_subtype {X : Type u_1} {L : Sublattice (Set X)} {T : ↥L} {x : X} :
x ∈ L.subtype T ↔ x ∈ T
source
@[simp]
theorem Sublattice.setLike_mem_inf {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L} {x : X} :
x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
source
@[simp]
theorem Sublattice.setLike_mem_sup {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L} {x : X} :
x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T
source
@[simp]
theorem Sublattice.setLike_mem_coe {X : Type u_1} {L : Sublattice (Set X)} {T : ↥L} {x : X} :
x ∈ ↑T ↔ x ∈ T
source
@[simp]
theorem Sublattice.setLike_mem_mk {X : Type u_1} {L : Sublattice (Set X)} {x : X} (U : Set X) (h : U ∈ L) :
x ∈ ⟨U, h⟩ ↔ x ∈ U
source
theorem CompleteSublattice.ext {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L} (h : ∀ (x : X), x ∈ S ↔ x ∈ T) :
S = T
source
theorem CompleteSublattice.mem_subtype {X : Type u_1} {L : CompleteSublattice (Set X)} {T : ↥L} {x : X} :
x ∈ L.subtype T ↔ x ∈ T
source
@[simp]
theorem CompleteSublattice.mem_inf {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L} {x : X} :
x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
source
@[simp]
theorem CompleteSublattice.mem_sInf {X : Type u_1} {L : CompleteSublattice (Set X)} {𝒮 : Set ↥L} {x : X} :
x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T
source
@[simp]
theorem CompleteSublattice.mem_iInf {X : Type u_1} {L : CompleteSublattice (Set X)} {I : Sort u_2} {f : I → ↥L} {x : X} :
x ∈ ⨅ (i : I), f i ↔ ∀ (i : I), x ∈ f i
source
@[simp]
theorem CompleteSublattice.mem_top {X : Type u_1} {L : CompleteSublattice (Set X)} {x : X} :
x ∈ ⊤
source
@[simp]
theorem CompleteSublattice.mem_sup {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L} {x : X} :
x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T
source
@[simp]
theorem CompleteSublattice.mem_sSup {X : Type u_1} {L : CompleteSublattice (Set X)} {𝒮 : Set ↥L} {x : X} :
x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T
source
@[simp]
theorem CompleteSublattice.mem_iSup {X : Type u_1} {L : CompleteSublattice (Set X)} {I : Sort u_2} {f : I → ↥L} {x : X} :
x ∈ ⨆ (i : I), f i ↔ ∃ (i : I), x ∈ f i
source
@[simp]
theorem CompleteSublattice.not_mem_bot {X : Type u_1} {L : CompleteSublattice (Set X)} {x : X} :
x ∉ ⊥
source
@[simp]
theorem CompleteSublattice.mem_mk {X : Type u_1} {L : CompleteSublattice (Set X)} {x : X} (U : Set X) (h : U ∈ L) :
x ∈ ⟨U, h⟩ ↔ x ∈ U