mem_iInf

Mathlib.Order.CompleteLattice.SetLike

URI: https://scilib.ai/kg/mathlib#CompleteSublattice.mem_iInf

English

In a CompleteSublattice, x ∈ iInf f ⇔ ∀ i, x ∈ f i for a family f.

Русский

Для семейства f: i → Sublattice, x ∈ iInf f эквивалентно ∀ i, x ∈ f i.

LaTeX

$$$x \\in iInf f \\iff \\forall i, x \\in f(i)$$$

Lean4

@[simp]
theorem mem_iInf : x ∈ ⨅ i : I, f i ↔ ∀ i : I, x ∈ f i := by simp [← mem_subtype]

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

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

Разделы

Аффилиация

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