continuousOn_to_generateFrom_iff — Mathlib

English

The continuity on s is equivalent to a pointwise condition with respect to a generateFrom topology on β.

Русский

Непрерывность на s эквивалентна локальным условиям в отношении топологии generateFrom на β.

LaTeX

$$$@ContinuousOn\\ f\\ s \\iff \\forall x \\in s, \\forall t \\in T, f(x) \\in t \\rightarrow f^{-1}(t) \\in 𝓝[s](x)$$$

Lean4

theorem continuousOn_to_generateFrom_iff {β : Type*} {T : Set (Set β)} {f : α → β} :
    @ContinuousOn α β _ (.generateFrom T) f s ↔ ∀ x ∈ s, ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x :=
  forall₂_congr fun x _ => by
    delta ContinuousWithinAt
    simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq, and_imp]
    exact forall_congr' fun t => forall_swap

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