mem_sInf — Mathlib

English

For any S ⊆ Subalgebra(A), and x ∈ A, x ∈ sInf S iff ∀ p ∈ S, x ∈ p.

Русский

Для множества S подпалгебр A справедливо: x ∈ sInf S тогда и только тогда, когда ∀ p ∈ S, x ∈ p.

LaTeX

$$$x \in sInf S \iff \forall p \in S, x \in p$$$

Lean4

theorem mem_sInf {S : Set (Subalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p := by
  simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

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