continuous_iff_Ici — Mathlib

English

A function f into α is continuous iff the preimage of every interval Ici a is closed.

Русский

Функция f в α непрерывна тогда и только тогда, когда прообраз каждого промежутка Ici a замкнут.

LaTeX

$$$\\text{Continuous}(f) \\iff \\forall a,\\ IsClosed(f^{-1}(Ici(a)))$$$

Lean4

/-- A function `f : β → α` with lower topology in the codomain is continuous
if and only if the preimage of every interval `Set.Ici a` is a closed set.
-/
theorem continuous_iff_Ici [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ a, IsClosed (f ⁻¹' (Ici a)) :=
  by
  obtain rfl := IsLower.topology_eq α
  simp [continuous_generateFrom_iff]

Похожие утверждения