mem_iInf — Mathlib

English

An element x belongs to the iInf of a family s if and only if x belongs to every member s(i).

Русский

Элемент x принадлежит iInf семейства s тогда и только тогда, когда x принадлежит каждому элементу s(i).

LaTeX

$$$x \in \bigwedge_i s(i) \iff \forall i, x \in s(i).$$$

Lean4

@[simp]
theorem mem_iInf {ι} {x : α} {s : ι → Closeds α} : x ∈ iInf s ↔ ∀ i, x ∈ s i := by simp [iInf]

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