Mathlib.Topology.Basic

TopologicalSpace.ofClosed definition

 {X : Type u} (T : Set (Set X)) (empty_mem : ∅ ∈ T) (sInter_mem : ∀ A, A ⊆ T → ⋂₀ A ∈ T)
  (union_mem : ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ B ∈ T) : TopologicalSpace X

Full source

/-- A constructor for topologies by specifying the closed sets,
and showing that they satisfy the appropriate conditions. -/
def TopologicalSpace.ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : ∅∅ ∈ T)
    (sInter_mem : ∀ A, A ⊆ T → ⋂₀ A⋂₀ A ∈ T)
    (union_mem : ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ BA ∪ B ∈ T) : TopologicalSpace X where
  IsOpen X := XᶜXᶜ ∈ T
  isOpen_univ := by simp [empty_mem]
  isOpen_inter s t hs ht := by simpa only [compl_inter] using union_mem sᶜ hs tᶜ ht
  isOpen_sUnion s hs := by
    simp only [Set.compl_sUnion]
    exact sInter_mem (complcompl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy

Topology generated by closed sets

Informal description

Given a type $X$ and a collection $T$ of subsets of $X$ satisfying: 1. The empty set is in $T$, 2. $T$ is closed under arbitrary intersections (i.e., for any subset $A \subseteq T$, the intersection $\bigcap A$ is in $T$), 3. $T$ is closed under finite unions (i.e., for any $A, B \in T$, the union $A \cup B$ is in $T$), then the function `TopologicalSpace.ofClosed` constructs a topology on $X$ where a set is open if and only if its complement is in $T$.

isOpen_mk theorem

{p h₁ h₂ h₃} : IsOpen[⟨p, h₁, h₂, h₃⟩] s ↔ p s

Full source

lemma isOpen_mk {p h₁ h₂ h₃} : IsOpen[⟨p, h₁, h₂, h₃⟩]IsOpen[⟨p, h₁, h₂, h₃⟩] s ↔ p s := Iff.rfl

Characterization of Open Sets in Generated Topology

Informal description

For a topological space defined by a collection of sets $T$ with properties $h₁$ (empty set is in $T$), $h₂$ (closed under arbitrary intersections), and $h₃$ (closed under finite unions), a set $s$ is open in this topology if and only if $s$ belongs to $T$.

TopologicalSpace.ext theorem

: ∀ {f g : TopologicalSpace X}, IsOpen[f] = IsOpen[g] → f = g

Full source

@[ext (iff := false)]
protected theorem TopologicalSpace.ext :
    ∀ {f g : TopologicalSpace X}, IsOpen[f] = IsOpen[g] → f = g
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl

Equality of Topological Spaces via Open Sets

Informal description

For any two topological space structures $f$ and $g$ on a type $X$, if their collections of open sets are equal, then the topological spaces are equal, i.e., $f = g$.

TopologicalSpace.ext_iff theorem

{t t' : TopologicalSpace X} : t = t' ↔ ∀ s, IsOpen[t] s ↔ IsOpen[t'] s

Full source

protected theorem TopologicalSpace.ext_iff {t t' : TopologicalSpace X} :
    t = t' ↔ ∀ s, IsOpen[t] s ↔ IsOpen[t'] s :=
  ⟨fun h _ => h ▸ Iff.rfl, fun h => by ext; exact h _⟩

Equality of Topological Spaces via Open Sets Criterion

Informal description

Two topological space structures $t$ and $t'$ on a type $X$ are equal if and only if for every subset $s$ of $X$, $s$ is open in $t$ if and only if $s$ is open in $t'$.

isOpen_fold theorem

{t : TopologicalSpace X} : t.IsOpen s = IsOpen[t] s

Full source

theorem isOpen_fold {t : TopologicalSpace X} : t.IsOpen s = IsOpen[t] s :=
  rfl

Equivalence of Topological Openness Predicates

Informal description

For a topological space $X$ with topology $t$, the predicate `t.IsOpen s` is equivalent to `IsOpen[t] s` for any subset $s$ of $X$.

isOpen_iUnion theorem

{f : ι → Set X} (h : ∀ i, IsOpen (f i)) : IsOpen (⋃ i, f i)

Full source

theorem isOpen_iUnion {f : ι → Set X} (h : ∀ i, IsOpen (f i)) : IsOpen (⋃ i, f i) :=
  isOpen_sUnion (forall_mem_range.2 h)

Openness of Arbitrary Union of Open Sets

Informal description

For any indexed family of sets $\{f_i\}_{i \in \iota}$ in a topological space $X$, if each $f_i$ is open, then their union $\bigcup_{i} f_i$ is also open.

isOpen_biUnion theorem

{s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋃ i ∈ s, f i)

Full source

theorem isOpen_biUnion {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) :
    IsOpen (⋃ i ∈ s, f i) :=
  isOpen_iUnion fun i => isOpen_iUnion fun hi => h i hi

Openness of Union over a Set of Open Sets

Informal description

For any set $s$ in a type $\alpha$ and any family of sets $\{f_i\}_{i \in \alpha}$ in a topological space $X$, if for every $i \in s$ the set $f_i$ is open, then the union $\bigcup_{i \in s} f_i$ is open.

IsOpen.union theorem

(h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∪ s₂)

Full source

theorem IsOpen.union (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∪ s₂) := by
  rw [union_eq_iUnion]; exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Union of Two Open Sets is Open

Informal description

For any two sets $s_1$ and $s_2$ in a topological space $X$, if both $s_1$ and $s_2$ are open, then their union $s_1 \cup s_2$ is also open.

isOpen_iff_of_cover theorem

{f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : (⋃ i, f i) = univ) : IsOpen s ↔ ∀ i, IsOpen (f i ∩ s)

Full source

lemma isOpen_iff_of_cover {f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : (⋃ i, f i) = univ) :
    IsOpenIsOpen s ↔ ∀ i, IsOpen (f i ∩ s) := by
  refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩
  rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]
  exact isOpen_iUnion fun i ↦ h i

Openness Criterion via Open Cover: $s$ is open $\iff$ all $f_i \cap s$ are open

Informal description

Let $\{f_i\}_{i \in \alpha}$ be a family of open sets in a topological space $X$ such that their union covers $X$ (i.e., $\bigcup_i f_i = X$). Then a subset $s \subseteq X$ is open if and only if for every $i \in \alpha$, the intersection $f_i \cap s$ is open.

isOpen_empty theorem

: IsOpen (∅ : Set X)

Full source

@[simp] theorem isOpen_empty : IsOpen (∅ : Set X) := by
  rw [← sUnion_empty]; exact isOpen_sUnion fun a => False.elim

Openness of the Empty Set

Informal description

The empty set is open in any topological space $X$.

Set.Finite.isOpen_sInter theorem

{s : Set (Set X)} (hs : s.Finite) (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋂₀ s)

Full source

theorem Set.Finite.isOpen_sInter {s : Set (Set X)} (hs : s.Finite) (h : ∀ t ∈ s, IsOpen t) :
    IsOpen (⋂₀ s) := by
  induction s, hs using Set.Finite.induction_on with
  | empty => rw [sInter_empty]; exact isOpen_univ
  | insert _ _ ih =>
    simp only [sInter_insert, forall_mem_insert] at h ⊢
    exact h.1.inter (ih h.2)

Finite Intersection of Open Sets is Open

Informal description

For any finite collection $\{U_i\}_{i \in I}$ of open sets in a topological space $X$, the intersection $\bigcap_{i \in I} U_i$ is open.

Set.Finite.isOpen_biInter theorem

{s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i)

Full source

theorem Set.Finite.isOpen_biInter {s : Set α} {f : α → Set X} (hs : s.Finite)
    (h : ∀ i ∈ s, IsOpen (f i)) :
    IsOpen (⋂ i ∈ s, f i) :=
  sInter_image f s ▸ (hs.image _).isOpen_sInter (forall_mem_image.2 h)

Finite Intersection of Open Sets is Open (Indexed Version)

Informal description

For any finite set $s \subseteq \alpha$ and any family of open sets $\{f(i)\}_{i \in s}$ in a topological space $X$, the intersection $\bigcap_{i \in s} f(i)$ is open.

isOpen_iInter_of_finite theorem

[Finite ι] {s : ι → Set X} (h : ∀ i, IsOpen (s i)) : IsOpen (⋂ i, s i)

Full source

theorem isOpen_iInter_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsOpen (s i)) :
    IsOpen (⋂ i, s i) :=
  (finite_range _).isOpen_sInter (forall_mem_range.2 h)

Finite Intersection of Open Sets is Open (Indexed Version)

Informal description

For a finite index type $\iota$ and a family of open sets $\{s_i\}_{i \in \iota}$ in a topological space $X$, the intersection $\bigcap_{i \in \iota} s_i$ is open.

isOpen_biInter_finset theorem

{s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i)

Full source

theorem isOpen_biInter_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) :
    IsOpen (⋂ i ∈ s, f i) :=
  s.finite_toSet.isOpen_biInter h

Finite Intersection of Open Sets is Open (Finset Version)

Informal description

For any finite set $s$ (represented as a finset) of type $\alpha$ and any family of open sets $\{f(i)\}_{i \in s}$ in a topological space $X$, the intersection $\bigcap_{i \in s} f(i)$ is open.

isOpen_const theorem

{p : Prop} : IsOpen {_x : X | p}

Full source

@[simp]
theorem isOpen_const {p : Prop} : IsOpen { _x : X | p } := by by_cases p <;> simp [*]

Constant Predicate Sets are Open

Informal description

For any proposition $p$, the set $\{x \in X \mid p\}$ is open in the topological space $X$.

IsOpen.and theorem

: IsOpen {x | p₁ x} → IsOpen {x | p₂ x} → IsOpen {x | p₁ x ∧ p₂ x}

Full source

theorem IsOpen.and : IsOpen { x | p₁ x } → IsOpen { x | p₂ x } → IsOpen { x | p₁ x ∧ p₂ x } :=
  IsOpen.inter

Intersection of Open Sets Defined by Predicates is Open

Informal description

If two sets $\{x \mid p_1(x)\}$ and $\{x \mid p_2(x)\}$ are open in a topological space $X$, then their intersection $\{x \mid p_1(x) \land p_2(x)\}$ is also open.

isOpen_compl_iff theorem

: IsOpen sᶜ ↔ IsClosed s

Full source

@[simp] theorem isOpen_compl_iff : IsOpenIsOpen sᶜ ↔ IsClosed s :=
  ⟨fun h => ⟨h⟩, fun h => h.isOpen_compl⟩

Open Complement Characterization of Closed Sets

Informal description

For any subset $s$ of a topological space, the complement $s^c$ is open if and only if $s$ is closed.

TopologicalSpace.ext_iff_isClosed theorem

{X} {t₁ t₂ : TopologicalSpace X} : t₁ = t₂ ↔ ∀ s, IsClosed[t₁] s ↔ IsClosed[t₂] s

Full source

theorem TopologicalSpace.ext_iff_isClosed {X} {t₁ t₂ : TopologicalSpace X} :
    t₁ = t₂ ↔ ∀ s, IsClosed[t₁] s ↔ IsClosed[t₂] s := by
  rw [TopologicalSpace.ext_iff, compl_surjective.forall]
  simp only [@isOpen_compl_iff _ _ t₁, @isOpen_compl_iff _ _ t₂]

Equality of Topological Spaces via Closed Sets Criterion

Informal description

Two topological space structures $t_1$ and $t_2$ on a set $X$ are equal if and only if for every subset $s \subseteq X$, $s$ is closed in $t_1$ if and only if $s$ is closed in $t_2$.

isClosed_const theorem

{p : Prop} : IsClosed {_x : X | p}

Full source

theorem isClosed_const {p : Prop} : IsClosed { _x : X | p } := ⟨isOpen_const (p := ¬p)⟩

Constant Predicate Sets are Closed

Informal description

For any proposition $p$, the set $\{x \in X \mid p\}$ is closed in the topological space $X$.

isClosed_empty theorem

: IsClosed (∅ : Set X)

Full source

@[simp] theorem isClosed_empty : IsClosed (∅ : Set X) := isClosed_const

The Empty Set is Closed

Informal description

The empty set $\emptyset$ is closed in any topological space $X$.

isClosed_univ theorem

: IsClosed (univ : Set X)

Full source

@[simp] theorem isClosed_univ : IsClosed (univ : Set X) := isClosed_const

The Universal Set is Closed in Any Topological Space

Informal description

The universal set $X$ (the set containing all points of the topological space $X$) is closed in $X$.

IsOpen.isLocallyClosed theorem

(hs : IsOpen s) : IsLocallyClosed s

Full source

lemma IsOpen.isLocallyClosed (hs : IsOpen s) : IsLocallyClosed s :=
  ⟨_, _, hs, isClosed_univ, (inter_univ _).symm⟩

Open Sets are Locally Closed

Informal description

If a set $s$ in a topological space is open, then it is locally closed, meaning that for every point $x \in s$, there exists a neighborhood $U$ of $x$ such that $s \cap U$ is closed in $U$.

IsClosed.isLocallyClosed theorem

(hs : IsClosed s) : IsLocallyClosed s

Full source

lemma IsClosed.isLocallyClosed (hs : IsClosed s) : IsLocallyClosed s :=
  ⟨_, _, isOpen_univ, hs, (univ_inter _).symm⟩

Closed Sets are Locally Closed

Informal description

If a set $s$ in a topological space $X$ is closed, then it is locally closed.

IsClosed.union theorem

: IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)

Full source

theorem IsClosed.union : IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂) := by
  simpa only [← isOpen_compl_iff, compl_union] using IsOpen.inter

Closedness Under Finite Unions

Informal description

If two sets $s_1$ and $s_2$ in a topological space are closed, then their union $s_1 \cup s_2$ is also closed.

isClosed_sInter theorem

{s : Set (Set X)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s)

Full source

theorem isClosed_sInter {s : Set (Set X)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s) := by
  simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion

Closedness of Arbitrary Intersections of Closed Sets

Informal description

For any family of sets $s \subseteq \mathcal{P}(X)$ in a topological space $X$, if every set $t \in s$ is closed, then the intersection $\bigcap_{t \in s} t$ is closed.

isClosed_iInter theorem

{f : ι → Set X} (h : ∀ i, IsClosed (f i)) : IsClosed (⋂ i, f i)

Full source

theorem isClosed_iInter {f : ι → Set X} (h : ∀ i, IsClosed (f i)) : IsClosed (⋂ i, f i) :=
  isClosed_sInter <| forall_mem_range.2 h

Closedness of Arbitrary Intersections of Closed Sets (Indexed Version)

Informal description

For any indexed family of sets $\{f_i\}_{i \in \iota}$ in a topological space $X$, if each set $f_i$ is closed, then the intersection $\bigcap_{i \in \iota} f_i$ is closed.

isClosed_biInter theorem

{s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋂ i ∈ s, f i)

Full source

theorem isClosed_biInter {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) :
    IsClosed (⋂ i ∈ s, f i) :=
  isClosed_iInter fun i => isClosed_iInter <| h i

Closedness of Bounded Intersections of Closed Sets

Informal description

Let $X$ be a topological space and $\alpha$ be a type. For any subset $s \subseteq \alpha$ and any family of sets $\{f_i\}_{i \in \alpha}$ in $X$, if each $f_i$ is closed for all $i \in s$, then the intersection $\bigcap_{i \in s} f_i$ is closed.

isClosed_compl_iff theorem

{s : Set X} : IsClosed sᶜ ↔ IsOpen s

Full source

@[simp]
theorem isClosed_compl_iff {s : Set X} : IsClosedIsClosed sᶜ ↔ IsOpen s := by
  rw [← isOpen_compl_iff, compl_compl]

Closed Complement Characterization of Open Sets

Informal description

For any subset $s$ of a topological space $X$, the complement $s^c$ is closed if and only if $s$ is open.

IsOpen.sdiff theorem

(h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t)

Full source

theorem IsOpen.sdiff (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t) :=
  IsOpen.inter h₁ h₂.isOpen_compl

Openness of Set Difference Between Open and Closed Sets

Informal description

Let $X$ be a topological space. If $s$ is an open set and $t$ is a closed set in $X$, then the set difference $s \setminus t$ is open.

IsClosed.inter theorem

(h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ∩ s₂)

Full source

theorem IsClosed.inter (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ∩ s₂) := by
  rw [← isOpen_compl_iff] at *
  rw [compl_inter]
  exact IsOpen.union h₁ h₂

Intersection of Two Closed Sets is Closed

Informal description

For any two subsets $s_1$ and $s_2$ of a topological space, if both $s_1$ and $s_2$ are closed, then their intersection $s_1 \cap s_2$ is also closed.

IsClosed.sdiff theorem

(h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t)

Full source

theorem IsClosed.sdiff (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t) :=
  IsClosed.inter h₁ (isClosed_compl_iff.mpr h₂)

Closedness of Set Difference Between Closed and Open Sets

Informal description

For any subsets $s$ and $t$ of a topological space $X$, if $s$ is closed and $t$ is open, then the set difference $s \setminus t$ is closed.

Set.Finite.isClosed_biUnion theorem

{s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋃ i ∈ s, f i)

Full source

theorem Set.Finite.isClosed_biUnion {s : Set α} {f : α → Set X} (hs : s.Finite)
    (h : ∀ i ∈ s, IsClosed (f i)) :
    IsClosed (⋃ i ∈ s, f i) := by
  simp only [← isOpen_compl_iff, compl_iUnion] at *
  exact hs.isOpen_biInter h

Finite Union of Closed Sets is Closed (Indexed Version)

Informal description

For any finite set $s$ in a type $\alpha$ and any family of closed sets $\{f(i)\}_{i \in s}$ in a topological space $X$, the union $\bigcup_{i \in s} f(i)$ is closed.

isClosed_biUnion_finset theorem

{s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋃ i ∈ s, f i)

Full source

lemma isClosed_biUnion_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) :
    IsClosed (⋃ i ∈ s, f i) :=
  s.finite_toSet.isClosed_biUnion h

Finite Union of Closed Sets is Closed (Finset Version)

Informal description

For any finite set $s$ (represented as a finset) in a type $\alpha$ and any family of closed sets $\{f(i)\}_{i \in s}$ in a topological space $X$, the union $\bigcup_{i \in s} f(i)$ is closed.

isClosed_iUnion_of_finite theorem

[Finite ι] {s : ι → Set X} (h : ∀ i, IsClosed (s i)) : IsClosed (⋃ i, s i)

Full source

theorem isClosed_iUnion_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsClosed (s i)) :
    IsClosed (⋃ i, s i) := by
  simp only [← isOpen_compl_iff, compl_iUnion] at *
  exact isOpen_iInter_of_finite h

Finite Union of Closed Sets is Closed (Indexed Version)

Informal description

For a finite index type $\iota$ and a family of closed sets $\{s_i\}_{i \in \iota}$ in a topological space $X$, the union $\bigcup_{i \in \iota} s_i$ is closed.

isClosed_imp theorem

{p q : X → Prop} (hp : IsOpen {x | p x}) (hq : IsClosed {x | q x}) : IsClosed {x | p x → q x}

Full source

theorem isClosed_imp {p q : X → Prop} (hp : IsOpen { x | p x }) (hq : IsClosed { x | q x }) :
    IsClosed { x | p x → q x } := by
  simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq

Closedness of Implication Set under Open and Closed Conditions

Informal description

Let $X$ be a topological space and $p, q : X \to \text{Prop}$ be predicates on $X$. If the set $\{x \mid p(x)\}$ is open and the set $\{x \mid q(x)\}$ is closed, then the set $\{x \mid p(x) \to q(x)\}$ is closed.

IsClosed.not theorem

: IsClosed {a | p a} → IsOpen {a | ¬p a}

Full source

theorem IsClosed.not : IsClosed { a | p a } → IsOpen { a | ¬p a } :=
  isOpen_compl_iff.mpr

Openness of Complement from Closedness of Set

Informal description

If the set $\{a \mid p(a)\}$ is closed in a topological space, then the set $\{a \mid \neg p(a)\}$ is open.

le_nhds_lim theorem

{f : Filter X} (h : ∃ x, f ≤ 𝓝 x) : f ≤ 𝓝 (@lim _ _ (nonempty_of_exists h) f)

Full source

/-- If a filter `f` is majorated by some `𝓝 x`, then it is majorated by `𝓝 (Filter.lim f)`. We
formulate this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for
types without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify
this instance with any other instance. -/
theorem le_nhds_lim {f : Filter X} (h : ∃ x, f ≤ 𝓝 x) : f ≤ 𝓝 (@lim _ _ (nonempty_of_exists h) f) :=
  Classical.epsilon_spec h

Filter Limit Majorizes Original Filter

Informal description

Let $X$ be a topological space and $f$ a filter on $X$. If there exists a point $x \in X$ such that $f$ is finer than the neighborhood filter $\mathcal{N}(x)$, then $f$ is also finer than the neighborhood filter of the limit point $\lim f$.

tendsto_nhds_limUnder theorem

 {f : Filter α} {g : α → X} (h : ∃ x, Tendsto g f (𝓝 x)) : Tendsto g f (𝓝 (@limUnder _ _ _ (nonempty_of_exists h) f g))

Full source

/-- If `g` tends to some `𝓝 x` along `f`, then it tends to `𝓝 (Filter.limUnder f g)`. We formulate
this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for types
without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify this
instance with any other instance. -/
theorem tendsto_nhds_limUnder {f : Filter α} {g : α → X} (h : ∃ x, Tendsto g f (𝓝 x)) :
    Tendsto g f (𝓝 (@limUnder _ _ _ (nonempty_of_exists h) f g)) :=
  le_nhds_lim h

Limit of Function Along Filter Equals Limit Point

Informal description

Let $X$ be a topological space, $\alpha$ a type, $f$ a filter on $\alpha$, and $g : \alpha \to X$ a function. If there exists a point $x \in X$ such that $g$ tends to $x$ along $f$ (i.e., $\text{Tendsto}\, g\, f\, (\mathcal{N}(x))$), then $g$ tends to the limit point $\text{limUnder}\, f\, g$ along $f$ (i.e., $\text{Tendsto}\, g\, f\, (\mathcal{N}(\text{limUnder}\, f\, g))$).

limUnder_of_not_tendsto theorem

 [hX : Nonempty X] {f : Filter α} {g : α → X} (h : ¬∃ x, Tendsto g f (𝓝 x)) : limUnder f g = Classical.choice hX

Full source

theorem limUnder_of_not_tendsto [hX : Nonempty X] {f : Filter α} {g : α → X}
    (h : ¬ ∃ x, Tendsto g f (𝓝 x)) :
    limUnder f g = Classical.choice hX := by
  simp_rw [Tendsto] at h
  simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]

Limit of Function Along Filter When No Limit Exists

Informal description

Let $X$ be a nonempty topological space, $α$ be a type, $f$ be a filter on $α$, and $g : α → X$ be a function. If there does not exist any point $x \in X$ such that $g$ tends to $x$ along $f$, then the limit of $g$ along $f$ is equal to an arbitrary chosen point in $X$.

Mathlib.Topology.Basic

Implementation notes

References

Tags