frequently_curry_iff — Mathlib

English

The frequent version of curry: (∃ᶠ 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

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

Lean4

theorem frequently_curry_iff (p : (α × β) → Prop) : (∃ᶠ x in l.curry m, p x) ↔ ∃ᶠ x in l, ∃ᶠ y in m, p (x, y) := by
  simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]

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