basis_left — Mathlib

English

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

Русский

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

LaTeX

$$$ H : Tendsto f\ la lb \Rightarrow \forall t \in lb, \exists i, pa i \land MapsTo f (sa i) t $$$

Lean4

theorem basis_left (H : Tendsto f la lb) (hla : la.HasBasis pa sa) : ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t :=
  hla.tendsto_left_iff.1 H

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