mem_sInf — Mathlib

English

An element x belongs to the infimum of a set S of closed subsets exactly when x belongs to every member of S.

Русский

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

LaTeX

$$$x \in sInf(S) \iff \forall C \in S, x \in C.$$$

Lean4

@[simp]
theorem mem_sInf {S : Set (Closeds α)} {x : α} : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s :=
  mem_iInter₂

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