Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit d04fff9

Browse files
committed
feat(topology/{order,separation}): several lemmas from an old branch (#12794)
* add `mem_nhds_discrete`; * replace the proof of `is_open_implies_is_open_iff` by `iff.rfl`; * add lemmas about `separated`.
1 parent 7f1ba1a commit d04fff9

File tree

2 files changed

+25
-1
lines changed

2 files changed

+25
-1
lines changed

src/topology/order.lean

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,7 @@ instance : complete_lattice (topological_space α) :=
234234

235235
lemma is_open_implies_is_open_iff {a b : topological_space α} :
236236
(∀ s, a.is_open s → b.is_open s) ↔ b ≤ a :=
237-
@galois_insertion.u_le_u_iff _ (order_dual (topological_space α)) _ _ _ _ (gi_generate_from α) a b
237+
iff.rfl
238238

239239
/-- A topological space is discrete if every set is open, that is,
240240
its topology equals the discrete topology `⊥`. -/
@@ -268,6 +268,10 @@ end
268268
lemma nhds_discrete (α : Type*) [topological_space α] [discrete_topology α] : (@nhds α _) = pure :=
269269
(discrete_topology.eq_bot α).symm ▸ nhds_bot α
270270

271+
lemma mem_nhds_discrete [topological_space α] [discrete_topology α] {x : α} {s : set α} :
272+
s ∈ 𝓝 x ↔ x ∈ s :=
273+
by rw [nhds_discrete, mem_pure]
274+
271275
lemma le_of_nhds_le_nhds {t₁ t₂ : topological_space α} (h : ∀x, @nhds α t₁ x ≤ @nhds α t₂ x) :
272276
t₁ ≤ t₂ :=
273277
assume s, show @is_open α t₂ s → @is_open α t₁ s,

src/topology/separation.lean

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,12 +114,32 @@ open separated
114114
lemma comm (s t : set α) : separated s t ↔ separated t s :=
115115
⟨symm, symm⟩
116116

117+
lemma preimage [topological_space β] {f : α → β} {s t : set β} (h : separated s t)
118+
(hf : continuous f) : separated (f ⁻¹' s) (f ⁻¹' t) :=
119+
let ⟨U, V, oU, oV, sU, tV, UV⟩ := h in
120+
⟨f ⁻¹' U, f ⁻¹' V, oU.preimage hf, oV.preimage hf, preimage_mono sU, preimage_mono tV,
121+
UV.preimage f⟩
122+
123+
protected lemma disjoint {s t : set α} (h : separated s t) : disjoint s t :=
124+
let ⟨U, V, hU, hV, hsU, htV, hd⟩ := h in hd.mono hsU htV
125+
126+
lemma disjoint_closure_left {s t : set α} (h : separated s t) : disjoint (closure s) t :=
127+
let ⟨U, V, hU, hV, hsU, htV, hd⟩ := h
128+
in (hd.closure_left hV).mono (closure_mono hsU) htV
129+
130+
lemma disjoint_closure_right {s t : set α} (h : separated s t) : disjoint s (closure t) :=
131+
h.symm.disjoint_closure_left.symm
132+
117133
lemma empty_right (a : set α) : separated a ∅ :=
118134
⟨_, _, is_open_univ, is_open_empty, λ a h, mem_univ a, λ a h, by cases h, disjoint_empty _⟩
119135

120136
lemma empty_left (a : set α) : separated ∅ a :=
121137
(empty_right _).symm
122138

139+
lemma mono {s₁ s₂ t₁ t₂ : set α} (h : separated s₂ t₂) (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
140+
separated s₁ t₁ :=
141+
let ⟨U, V, hU, hV, hsU, htV, hd⟩ := h in ⟨U, V, hU, hV, hs.trans hsU, ht.trans htV, hd⟩
142+
123143
lemma union_left {a b c : set α} : separated a c → separated b c → separated (a ∪ b) c :=
124144
λ ⟨U, V, oU, oV, aU, bV, UV⟩ ⟨W, X, oW, oX, aW, bX, WX⟩,
125145
⟨U ∪ W, V ∩ X, is_open.union oU oW, is_open.inter oV oX,

0 commit comments

Comments
 (0)