English
For every α, if IsLawson α holds, then lawsonBasis α is a topological basis.
Русский
Пусть α удовлетворяет условию IsLawson, тогда lawsonBasis α является топологическим базисом.
LaTeX
$$$\forall \alpha,\ IsLawson(\alpha) \Rightarrow \text{TopologicalSpace.IsTopologicalBasis}(\operatorname{lawsonBasis}(\alpha)).$$$
Lean4
protected theorem isTopologicalBasis : TopologicalSpace.IsTopologicalBasis (lawsonBasis α) :=
by
have lawsonBasis_image2 :
lawsonBasis α =
(image2 (fun x x_1 ↦ ⇑WithLower.toLower ⁻¹' x ∩ ⇑WithScott.toScott ⁻¹' x_1) (IsLower.lowerBasis (WithLower α))
{U | IsOpen[scott α univ] U}) :=
by
rw [lawsonBasis, image2, IsLower.lowerBasis]
simp_rw [diff_eq_compl_inter]
aesop
rw [lawsonBasis_image2]
convert
IsTopologicalBasis.inf_induced IsLower.isTopologicalBasis (isTopologicalBasis_opens (α := WithScott α))
WithLower.toLower WithScott.toScott
rw [@topology_eq_lawson α _ _ _, lawson]
apply (congrArg₂ min _) _
· letI _ := lower α
exact (@IsLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩).isInducing.eq_induced
· letI _ := scott α univ
exact (@IsScott.withScottHomeomorph α _ (scott α univ) ⟨rfl⟩).isInducing.eq_induced
