prod_mem_curry

Mathlib.Order.Filter.Curry

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

English

If s ∈ l and t ∈ m then the product set s × t belongs to the curry of l and m.

Русский

Если s ∈ l и t ∈ m, то s × t ∈ l.curry m.

LaTeX

$$$\forall {l:Filter\ α} {m:Filter\ β} {s:Set\ α} {t:Set\ β}, s \in l ∧ t \in m \Rightarrow s \times t \in l.curry m$$

Lean4

theorem prod_mem_curry (hs : s ∈ l) (ht : t ∈ m) : s ×ˢ t ∈ l.curry m :=
  curry_le_prod <| prod_mem_prod hs ht

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

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

Разделы

Аффилиация

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