Skip to content

Commit

Permalink
doc(topology/separation): two typos (#10382)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Nov 19, 2021
1 parent e8858fd commit 7638fe2
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/topology/separation.lean
Expand Up @@ -50,7 +50,7 @@ This file defines the predicate `separated`, and common separation axioms
* `t2_iff_nhds`: A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.
* `t2_iff_is_closed_diagonal`: A space is T₂ iff the `diagonal` of `α` (that is, the set of all
points of the form `(a, a) : α × α`) is closed under the product topology.
* `finset_disjoing_finset_opens_of_t2`: Any two disjoint finsets are `separated`.
* `finset_disjoint_finset_opens_of_t2`: Any two disjoint finsets are `separated`.
* Most topological constructions preserve Hausdorffness;
these results are part of the typeclass inference system (e.g. `embedding.t2_space`)
* `set.eq_on.closure`: If two functions are equal on some set `s`, they are equal on its closure.
Expand Down Expand Up @@ -581,7 +581,7 @@ lemma tendsto_const_nhds_iff [t2_space α] {l : filter α} [ne_bot l] {c d : α}
⟨λ h, tendsto_nhds_unique (tendsto_const_nhds) h, λ h, h ▸ tendsto_const_nhds⟩

/-- A T₂.₅ space, also known as a Urysohn space, is a topological space
where for every pair `x ≠ y`, there are two open sets, with the intersection of clousures
where for every pair `x ≠ y`, there are two open sets, with the intersection of closures
empty, one containing `x` and the other `y` . -/
class t2_5_space (α : Type u) [topological_space α]: Prop :=
(t2_5 : ∀ x y (h : x ≠ y), ∃ (U V: set α), is_open U ∧ is_open V ∧
Expand Down

0 comments on commit 7638fe2

Please sign in to comment.