eventually_curry_iff — Mathlib

English

The equivalence between eventual curry statements: (∀ᶠ x in l.curry m, p x) ⇔ (∀ᶠ x in l, ∀ᶠ y in m, p (x, y)).

Русский

Эквивалентность выражений с предикатом curry: (∀ᶠ x в l.curry m, p x) ⇔ (∀ᶠ x в l, ∀ᶠ y в m, p (x, y)).

LaTeX

$$$(\\forall\\mathrm{ᶠ}\ x\\in l.curry m,\ p\ x) \\iff (\\forall\\mathrm{ᶠ}\\ x\\in l,\ \\forall\\mathrm{ᶠ}\\ y\\in m,\ p\\ (x,y))$$$

Lean4

theorem eventually_curry_iff {p : α × β → Prop} :
    (∀ᶠ x : α × β in l.curry m, p x) ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, p (x, y) :=
  Iff.rfl

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