mem_iInf — Mathlib

English

An element x is in the infimum of a family if and only if x belongs to every member of the family.

Русский

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

LaTeX

$$$$ x \in \bigwedge_{i} S_i \iff \forall i, x \in S_i $$$$

Lean4

theorem mem_iInf {ι : Sort*} {S : ι → L.Substructure M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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