mem_curry_iff

Mathlib.Order.Filter.Curry

URI: https://scilib.ai/kg/mathlib#Filter.mem_curry_iff

English

Mem Curry: s ∈ l.curry m ↔ ∀ᶠ x ∈ l, ∀ᶠ y ∈ m, (x,y) ∈ s.

Русский

Членство в curry: s ∈ l.curry m ⇔ ∀ᶠ x∈l, ∀ᶠ y∈m, (x,y) ∈ s.

LaTeX

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

Lean4

theorem mem_curry_iff {s : Set (α × β)} : s ∈ l.curry m ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, (x, y) ∈ s :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru