mem_infs

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.mem_infs

English

For any c, c belongs to s ⊼ t if and only if there exist a ∈ s and b ∈ t with a ⊓ b = c.

Русский

Членство элемента c в s ⊼ t эквивалентно существованию a ∈ s и b ∈ t таких, что a ⊓ b = c.

LaTeX

$$$ c \in s ⊼ t \iff \exists a \in s, \exists b \in t, a \sqcap b = c $$$

Lean4

@[simp]
theorem mem_infs : c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c := by simp [(· ⊼ ·)]

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

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

Разделы

Аффилиация

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