equivIco — Mathlib

English

General version: for hp: 0<p and x>0, (QuotientAddGroup.mk x) = 0 iff ∃ n ∈ ℕ with x = n·p.

Русский

Обобщённая версия: при hp: 0<p и x>0, (mk x) = 0 тогда и только тогда, когда существует n ∈ ℕ, x = n·p.

LaTeX

$$$$ hp: 0 < p \Rightarrow (0 < x) \Rightarrow \left( \operatorname{QuotientAddGroup.mk} x = 0 \iff \exists n \in \mathbb{N}, n \cdot p = x \right) $$$$

Lean4

/-- The equivalence between `AddCircle p` and the half-open interval `[a, a + p)`, whose inverse
is the natural quotient map. -/
def equivIco : AddCircle p ≃ Ico a (a + p) :=
  QuotientAddGroup.equivIcoMod hp.out a

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