rtendsto'_def — Mathlib

English

RTendsto' r l1 l2 is equivalent to saying that for every s ∈ l2, the set r.preimage s belongs to l1.

Русский

RTendsto' r l1 l2 эквивалентно тому, что для каждого s ∈ l2 множество r.preimage s принадлежит l1.

LaTeX

$$$ RTendsto'\\, r\\, l_1\\, l_2 \\iff \\forall s\\in l_2,\\ r.preimage s\\in l_1 $$$

Lean4

theorem rtendsto'_def (r : SetRel α β) (l₁ : Filter α) (l₂ : Filter β) :
    RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁ :=
  by
  unfold RTendsto' rcomap'; constructor
  · simpa [le_def, SetRel.mem_image] using fun h s hs => h _ _ hs Set.Subset.rfl
  · simpa [le_def, SetRel.mem_image] using fun h s t ht => mem_of_superset (h t ht)

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