English
In the closed-sets Galois connection, the closure operator applied to S equals hull(T, kernel(S)).
Русский
В связке замкнутых множеств по Галуа замыкание применительно к S равно hull(T, ker(S)).
LaTeX
$$$\\mathrm{gc\\_closureOperator}(S) = \\mathrm{hull}(T, \\ker(S)).$$$
Lean4
theorem closedsGC_closureOperator [TopologicalSpace α] [IsLower α] (hT : ∀ p ∈ T, InfPrime p) (hG : OrderGenerates T)
(S : Set T) : (TopologicalSpace.Closeds.gc (α := T)).closureOperator S = hull T (kernel S) :=
by
simp only [GaloisConnection.closureOperator_apply, Closeds.coe_closure, closure, le_antisymm_iff]
constructor
·
exact fun ⦃a⦄ a ↦
a (hull T (kernel S))
⟨(isClosed_iff hT).mpr ⟨kernel S, rfl⟩,
image_subset_iff.mp (fun _ hbS => CompleteSemilatticeInf.sInf_le _ _ hbS)⟩
· simp_rw [le_eq_subset, subset_sInter_iff]
intro R hR
rw [← (hull_kernel_of_isClosed hT hG hR.1), ← gc_closureOperator]
exact ClosureOperator.monotone _ hR.2
