mem_iInf — Mathlib

English

For a family S: ι → Subfield K and x ∈ K, x ∈ ⨅ i, S i iff ∀ i, x ∈ S i.

Русский

Для семейства S i и элемента x ∈ K: x ∈ ⨅ i, S i тогда и только тогда, когда ∀ i, x ∈ S i.

LaTeX

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

Lean4

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

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