mem_iInf — Mathlib

English

Simplicial simplification: membership in iInf is equivalent to pointwise membership across the system.

Русский

Упрощение: членство в iInf эквивалентно точечной членности по всем элементам индекса.

LaTeX

$$$x \\in \\iInf_i S_i \\iff \\forall i, x \\in S_i$$$

Lean4

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

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