mem_sInf — Mathlib

English

The membership in the infimum set sInf 𝒮 corresponds exactly to membership of each component of 𝒮.

Русский

Пользовательское свойство: x принадлежит sInf 𝒮 тогда и только тогда, когда для каждого компонента T ∈ 𝒮 x принадлежит T.

LaTeX

$$$x \\in sInf 𝒮 \\iff \\forall T \\in 𝒮, x \\in T$$$

Lean4

@[simp]
theorem mem_sInf : x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T := by simp [← mem_subtype]

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