continuous_iff_Iic — Mathlib

English

A function f: β → α with upper topology on α is continuous if and only if the preimage of every interval Iic a is closed.

Русский

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

LaTeX

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

Lean4

/-- A function `f : β → α` with upper topology in the codomain is continuous
if and only if the preimage of every interval `Set.Iic a` is a closed set. -/
theorem continuous_iff_Iic [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ a, IsClosed (f ⁻¹' (Iic a)) :=
  IsLower.continuous_iff_Ici (α := αᵒᵈ)

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