English
The image of a topological basis under an open quotient map is a topological basis.
Русский
Образ базиса при открытом квотIENT отображении является базисом.
LaTeX
$$$IsTopologicalBasis(Set.image π '' V)$, если $V$ — базис и $π$ — открытое отображение$$
Lean4
/-- The image of a topological basis under an open quotient map is a topological basis. -/
theorem isQuotientMap {V : Set (Set X)} (hV : IsTopologicalBasis V) (h' : IsQuotientMap π) (h : IsOpenMap π) :
IsTopologicalBasis (Set.image π '' V) :=
by
apply isTopologicalBasis_of_isOpen_of_nhds
· rintro - ⟨U, U_in_V, rfl⟩
apply h U (hV.isOpen U_in_V)
· intro y U y_in_U U_open
obtain ⟨x, rfl⟩ := h'.surjective y
let W := π ⁻¹' U
have x_in_W : x ∈ W := y_in_U
have W_open : IsOpen W := U_open.preimage h'.continuous
obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open
have XZ_in_U : π '' Z ⊆ U := (Set.image_mono Z_in_W).trans (image_preimage_subset π U)
exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, XZ_in_U⟩
