rtendsto_def — Mathlib

English

Equivalence: RTendsto r l1 l2 is equivalent to saying that for every s ∈ l2, r.core s ∈ l1.

Русский

Эквивалентность: RTendsto r l1 l2 эквивалентно тому, что для каждого s ∈ l2 верно r.core s ∈ l1.

LaTeX

$$$\mathrm{RTendsto}(r,l_1,l_2) \iff \forall s\in l_2, r.core s \in l_1$$$

Lean4

theorem rtendsto_def (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β) : RTendsto r l₁ l₂ ↔ ∀ s ∈ l₂, r.core s ∈ l₁ :=
  Iff.rfl

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