English
In the real numbers, inversion is a continuous map on the set of nonzero reals.
Русский
Обратная функция непрерывна на множестве ненулевых действительных чисел.
LaTeX
$$$\\text{Continuous }\\lambda a\\, (a \\in \\mathbb{R} \\setminus \\{0\\}) \\mapsto a^{-1}$$$
Lean4
/-- A set `s` is locally closed if one of the equivalent conditions below hold
1. It is the intersection of some open set and some closed set.
2. The coborder `(closure s \ s)ᶜ` is open.
3. `s` is closed in some neighborhood of `x` for all `x ∈ s`.
4. Every `x ∈ s` has some open neighborhood `U` such that `U ∩ closure s ⊆ s`.
5. `s` is open in the closure of `s`.
-/
theorem isLocallyClosed_tfae (s : Set X) :
List.TFAE
[IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)] :=
by
tfae_have 1 → 2 := by
rintro ⟨U, Z, hU, hZ, rfl⟩
have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
nth_rw 1 [← hZ.closure_eq]
rw [← compl_subset_iff_union, compl_subset_compl]
refine frontier_subset_closure.trans (closure_mono inter_subset_right)
rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this, inter_univ]
exact hU.union isClosed_frontier.isOpen_compl
tfae_have 2 → 3
| h, x => (⟨coborder s, h.mem_nhds <| subset_coborder ·, isClosed_preimage_val_coborder⟩)
tfae_have 3 → 4
| h, x, hx => by
obtain ⟨t, ht, ht'⟩ := h x hx
obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
rw [isClosed_preimage_val] at ht'
exact
⟨U, hxU, hU,
(subset_inter (inter_subset_left.trans hUt)
(hU.inter_closure.trans (closure_mono <| inter_subset_inter hUt subset_rfl))).trans
ht'⟩
tfae_have 4 → 5
| H => by
choose U hxU hU e using H
refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
· rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
exact e y hy ⟨hxU, x.2⟩
· exact (subset_iUnion₂ _ _ <| hxU x ·)
tfae_have 5 → 1
| H =>
by
convert H.isLocallyClosed.image IsInducing.subtypeVal (by simpa using isClosed_closure.isLocallyClosed)
simpa using subset_closure
tfae_finish
