English
The Lawson topology on a partial order is a T1 space.
Русский
Топология Lawson на частичном порядке является T1 пространством.
LaTeX
$$$\text{IsLawson}(\alpha) \Rightarrow T1Space(\alpha)$$$
Lean4
/-- The Lawson topology on a partial order is T₁. -/
-- see Note [lower instance priority]
instance (priority := 90) toT1Space : T1Space α where
t1
a := by
simp only [IsLawson.topology_eq_lawson]
rw [← (Set.OrdConnected.upperClosure_inter_lowerClosure ordConnected_singleton), ←
WithLawson.isClosed_preimage_ofLawson]
apply IsClosed.inter (lawsonClosed_of_lowerClosed _ (IsLower.isClosed_upperClosure (finite_singleton a)))
rw [lowerClosure_singleton, LowerSet.coe_Iic, ← WithLawson.isClosed_preimage_ofLawson]
exact lawsonClosed_of_scottClosed _ isClosed_Iic
