eventually_atTop_curry — Mathlib

English

Dual formulation of the curry principle for atTop with prod.

Русский

Дуальная формулировка карринга для atTop в сочетании с произведением.

LaTeX

$$$$ \text{See above, dual formulation for } atTop. $$$$

Lean4

theorem eventually_atTop_curry [Preorder α] [Preorder β] {p : α × β → Prop} (hp : ∀ᶠ x : α × β in Filter.atTop, p x) :
    ∀ᶠ k in atTop, ∀ᶠ l in atTop, p (k, l) :=
  by
  rw [← prod_atTop_atTop_eq] at hp
  exact hp.curry

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