tendsto_principal_principal — Mathlib

English

For f, s ⊆ α and t ⊆ β, Tendsto f (principal s) (principal t) iff ∀ a ∈ s, f(a) ∈ t.

Русский

Для любой функции f и подмножеств s ⊆ α, t ⊆ β, Tendsto f (principal s) (principal t) эквивалентно ∀ a ∈ s, f(a) ∈ t.

LaTeX

$$$ \\operatorname{Tendsto} f (\\mathcal{P} s) (\\mathcal{P} t) \\iff \\forall a \\in s, f(a) \\in t $$$

Lean4

theorem tendsto_principal_principal {f : α → β} {s : Set α} {t : Set β} : Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t := by
  simp

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