Theorems · Theorem · general topology

Filter.TendstoIxxClass.tendsto_Ixx

∀ {α : Type u_1} {Ixx : α → α → Set α} {l₁ : Filter α} {l₂ : outParam (Filter α)}
  [self : Filter.TendstoIxxClass Ixx l₁ l₂], Filter.Tendsto (fun p => Ixx p.1 p.2) (l₁ ×ˢ l₁) l₂.smallSets

Function.uncurry Ixx tends to l₂.smallSets along l₁ ×ˢ l₁. In other words, for any s ∈ l₂ there exists t ∈ l₁ such that Ixx x y ⊆ s whenever x ∈ t and y ∈ t. Use lemmas like Filter.Tendsto.Icc instead.

Defined in

Mathlib.Order.Filter.Interval

Cited by

8 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Filter.TendstoIxxClass