mem_mk — Mathlib

English

Membership in the principal filter generated by an ideal I corresponds to membership of the dual element: x ∈ (⟨I⟩) ⇔ toDual x ∈ I.

Русский

Членство в главном фильтре, порождённом идеалом I, соответствует членству двойственного элемента: x ∈ (⟨I⟩) ⇔ toDual x ∈ I.

LaTeX

$$$$ x \\in (\\langle I \\rangle : PFilter P) \\iff toDual x \\in I. $$$$

Lean4

@[simp]
theorem mem_mk (x : P) (I : Ideal Pᵒᵈ) : x ∈ (⟨I⟩ : PFilter P) ↔ toDual x ∈ I :=
  Iff.rfl

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