English
The embedding stoneCechUnit is inducing.
Русский
Отображение stoneCechUnit индуктивно (индуцировано).
LaTeX
$$$[CompletelyRegularSpace X] \\Rightarrow IsInducing (stoneCechUnit : X \\to StoneCech X)$$$
Lean4
theorem isInducing_stoneCechUnit [CompletelyRegularSpace X] : IsInducing (stoneCechUnit : X → StoneCech X) :=
by
rw [isInducing_iff_nhds]
intro x
apply le_antisymm
· rw [← map_le_iff_le_comap]; exact continuous_stoneCechUnit.continuousAt
· simp_rw [le_nhds_iff, ((nhds_basis_opens _).comap _).mem_iff, and_assoc]
intro U hxU hU
obtain ⟨f, hf, efx, hfU⟩ := CompletelyRegularSpace.completely_regular_isOpen x U hU hxU
conv at hfU => equals Uᶜ ⊆ f ⁻¹' { 1 } => simp [EqOn, subset_def]
rw [← compl_subset_comm, ← preimage_compl, ← stoneCechExtend_extends hf, preimage_comp] at hfU
refine ⟨stoneCechExtend hf ⁻¹' { 1 }ᶜ, ?_, isOpen_compl_singleton.preimage (continuous_stoneCechExtend hf), hfU⟩
rw [mem_preimage, stoneCechExtend_stoneCechUnit, efx, mem_compl_iff, mem_singleton_iff]
simp
