mem_iInf — Mathlib

English

For a family of submonoids S i, an element x belongs to the iInf of the family iff x belongs to every S i.

Русский

Для семейства подпmonoids S_i, элемент x принадлежит iInf семейства тогда и только тогда, когда x принадлежит каждому S_i.

LaTeX

$$(x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i$$

Lean4

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

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