SetLike instance for elements of CompleteSublattice (Set X)

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

theorem Sublattice.ext_mem {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L} (h : ∀ (x : X), x ∈ S ↔ x ∈ T) : S = T

theorem Sublattice.ext_mem_iff {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L} : S = T ↔ ∀ (x : X), x ∈ S ↔ x ∈ T

theorem Sublattice.mem_subtype {X : Type u_1} {L : Sublattice (Set X)} {T : ↥L} {x : X} : x ∈ L.subtype T ↔ x ∈ T

@[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

@[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

@[simp]

theorem Sublattice.setLike_mem_coe {X : Type u_1} {L : Sublattice (Set X)} {T : ↥L} {x : X} : x ∈ ↑T ↔ x ∈ T

theorem CompleteSublattice.ext {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L} (h : ∀ (x : X), x ∈ S ↔ x ∈ T) : S = T

theorem CompleteSublattice.ext_iff {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L} : S = T ↔ ∀ (x : X), x ∈ S ↔ x ∈ T

theorem CompleteSublattice.mem_subtype {X : Type u_1} {L : CompleteSublattice (Set X)} {T : ↥L} {x : X} : x ∈ L.subtype T ↔ x ∈ T

@[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

@[simp]

theorem CompleteSublattice.mem_sInf {X : Type u_1} {L : CompleteSublattice (Set X)} {𝒮 : Set ↥L} {x : X} : x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T

@[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

@[simp]

theorem CompleteSublattice.mem_top {X : Type u_1} {L : CompleteSublattice (Set X)} {x : X} : x ∈ ⊤

@[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

@[simp]

theorem CompleteSublattice.mem_sSup {X : Type u_1} {L : CompleteSublattice (Set X)} {𝒮 : Set ↥L} {x : X} : x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T

@[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

@[simp]

theorem CompleteSublattice.notMem_bot {X : Type u_1} {L : CompleteSublattice (Set X)} {x : X} : x ∉ ⊥