hasIdealSupport_iff — Mathlib

English

A RingPreordering P has HasIdealSupport if and only if for all x,a ∈ R, a ∈ P and −a ∈ P implies x a ∈ P and −(x a) ∈ P.

Русский

У RingPreordering P есть HasIdealSupport тогда и только тогда, когда для всех x,a ∈ R, если a ∈ P и −a ∈ P, то x a ∈ P и −(x a) ∈ P.

LaTeX

$$$P.HasIdealSupport \\iff \\forall x,a\\in R, (a \\in P \\rightarrow -a \\in P \\rightarrow (x a \\in P \\land -(x a) \\in P))$$$

Lean4

theorem hasIdealSupport_iff : P.HasIdealSupport ↔ ∀ x a : R, a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
    where
  mp _ := by simpa [mem_supportAddSubgroup] using P.smul_mem_support
  mpr _ := ⟨by simpa [mem_supportAddSubgroup]⟩

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