tendsto_left_iff — Mathlib

English

If hla is a basis for la, then Tendsto f la lb is equivalent to: for every t ∈ lb there exists i with pa i and MapsTo f (sa i) t.

Русский

Если hla является базисом для la, то равносильно: Tendsto f la lb эквивалентно: для каждого t ∈ lb существует i с pa i и MapsTo f (sa i) t.

LaTeX

$$$ \text{Tendsto } f\ la\ lb \iff \forall t \in lb, \exists i, p(i) \land MapsTo f (sa i) t $$$

Lean4

theorem tendsto_left_iff (hla : la.HasBasis pa sa) : Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t :=
  by
  simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]
  rfl

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