English
Under a unique index for ι, IsCompactOpenCovered f U is equivalent to the existence of a single compact open V in the X connected to the unique default index by f.
Русский
При наличии единственного индекса для ι изоморфизм сохраняет: покрытие компактно-открыто через единственный компактно-открытый образ.
LaTeX
$$$IsCompactOpenCovered f U \iff \exists V : Opens(X_{Unique.instInhabited.default}), IsCompact V.1 \wedge f Unique.instInhabited.default '' V.1 = U.$$$
Lean4
theorem iff_of_unique [Unique ι] :
IsCompactOpenCovered f U ↔ ∃ (V : Opens (X default)), IsCompact V.1 ∧ f default '' V.1 = U :=
by
refine ⟨fun ⟨s, hs, V, hc, hcov⟩ ↦ ?_, fun ⟨V, hc, h⟩ ↦ ?_⟩
· by_cases h : s = ∅
· aesop
· obtain rfl : s = { default } := by
rw [← Set.univ_unique, Subsingleton.eq_univ_of_nonempty (Set.nonempty_iff_ne_empty.mpr h)]
aesop
· refine ⟨{ default }, Set.finite_singleton _, fun i h ↦ h ▸ V, fun i ↦ ?_, by simpa⟩
rintro rfl
simpa
