mem_iInf — Mathlib

English

Let p : ι → LieSubmodule R L M. For x in M, x ∈ ⨅ i, p i iff ∀ i, x ∈ p i.

Русский

Пусть p : ι → LieSubmodule R L M. Для элемента x ∈ M верно: x ∈ ⨅ i, p i тогда и только тогда, когда для всех i выполняется x ∈ p i.

LaTeX

$$$x \in \bigwedge_{i} p_i \;\Longleftrightarrow\; \forall i, x \in p_i$$$

Lean4

@[simp]
theorem mem_iInf {ι} (p : ι → LieSubmodule R L M) {x} : (x ∈ ⨅ i, p i) ↔ ∀ i, x ∈ p i := by
  rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]; rfl

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