English
Let α be a semilattice with Inf and a topology, and T a subset of α such that every p in T is an InfPrime. Then the collection of complements of hulls, namely the sets of the form (hull(T, a))^c, forms a topological basis for the relative lower topology on T.
Русский
Пусть α — полупорядоченная структура сInf, имеется топология, T ⊆ α и для каждого p ∈ T выполняется InfPrime p. Тогда множество всех дополнений к оболочкам hull(T, a) образуют базис относительной нижней топологии на T.
LaTeX
$$$IsTopologicalBasis \\{S : Set T \\mid \\exists a, (hull(T, a))^{c} = S\\}$$$
Lean4
theorem isTopologicalBasis_relativeLower (hT : ∀ p ∈ T, InfPrime p) :
IsTopologicalBasis {S : Set T | ∃ (a : α), (hull T a)ᶜ = S} :=
by
convert isTopologicalBasis_subtype Topology.IsLower.isTopologicalBasis T
ext R
simp only [preimage_compl, mem_setOf_eq, IsLower.lowerBasis, mem_image, exists_exists_and_eq_and]
constructor <;> intro ha
· obtain ⟨a, ha'⟩ := ha
use { a }
rw [← (Function.Injective.preimage_image Subtype.val_injective R), ← ha']
simp only [finite_singleton, upperClosure_singleton, UpperSet.coe_Ici, image_val_compl, Subtype.image_preimage_coe,
diff_self_inter, preimage_diff, Subtype.coe_preimage_self, true_and]
exact compl_eq_univ_diff (Subtype.val ⁻¹' Ici a)
· obtain ⟨F, hF⟩ := ha
lift F to Finset α using hF.1
use Finset.inf F id
ext
simp [hull_finsetInf hT, ← hF.2]
