mem_iInf — Mathlib

English

For a family of subgroups S_i, x ∈ ⨅ i, S_i iff ∀ i, x ∈ S_i.

Русский

Для семейства подгрупп S_i верно: x ∈ ⨅ i, S_i тогда и только тогда, когда ∀ i, x ∈ S_i.

LaTeX

$$$x \in \bigwedge_{i} S_i \iff \forall i, x \in S_i$$$

Lean4

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

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