isStarProjection_one_sub_iff — Mathlib

English

IsStarProjection(1 − p) holds if and only if IsStarProjection(p) holds.

Русский

IsStarProjection(1 − p) выполняется тогда и только тогда, когда IsStarProjection(p) выполняется.

LaTeX

$$$ \text{IsStarProjection}(1 - p) \iff \text{IsStarProjection}(p). $$$

Lean4

theorem _root_.isStarProjection_one_sub_iff [StarRing R] : IsStarProjection (1 - p) ↔ IsStarProjection p :=
  ⟨fun h ↦ sub_sub_cancel 1 p ▸ h.one_sub, .one_sub⟩

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