ne_one_iff_exists — Mathlib

English

An element x of WithOne α is not equal to 1 if and only if there exists a ∈ α with the embedding equal to x.

Русский

Элемент x из WithOne α не равен единице тогда и только тогда, когда существует a ∈ α, такое что встроение совпадает с x.

LaTeX

$$$x \neq 1 \iff \exists a : α, \mathrm{WithOne.coe}\ a = x$$$

Lean4

@[to_additive]
theorem ne_one_iff_exists {x : WithOne α} : x ≠ 1 ↔ ∃ a : α, ↑a = x :=
  Option.ne_none_iff_exists

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