mem_ofZNum' — Mathlib

English

For all m: Num and n: ZNum, m ∈ ofZNum' n iff n = toZNum m.

Русский

Для всех m: Num и n: ZNum верно, что m принадлежит toZNum n тогда, когда n = toZNum m.

LaTeX

$$$$\forall m:\mathrm{Num},\forall n:\mathrm{ZNum},\ m \in \mathrm{ofZNum'}(n) \iff n = \mathrm{toZNum}(m).$$$$

Lean4

theorem mem_ofZNum' : ∀ {m : Num} {n : ZNum}, m ∈ ofZNum' n ↔ n = toZNum m
  | 0, 0 => ⟨fun _ => rfl, fun _ => rfl⟩
  | pos _, 0 => ⟨nofun, nofun⟩
  | m, ZNum.pos p => Option.some_inj.trans <| by cases m <;> constructor <;> intro h <;> try cases h <;> rfl
  | m, ZNum.neg p => ⟨nofun, fun h => by cases m <;> cases h⟩

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