mem_sInf_iff — Mathlib

English

Let α be a poset. For any set S of upper sets of α, a ∈ sInf S if and only if there exists an upper set s in S with a ∈ s.

Русский

Пусть α упорядочено.po; для любой семейства S верхних множеств α верно: a принадлежит infimum S тогда и только тогда, когда существует s ∈ S, такое что a ∈ s.

LaTeX

$$$ a \in sInf S \iff \exists s \in S, a \in s $$$

Lean4

@[simp]
theorem mem_sInf_iff : a ∈ sInf S ↔ ∃ s ∈ S, a ∈ s :=
  mem_iUnion₂.trans <| by simp only [exists_prop, SetLike.mem_coe]

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