ofNat_eq_map_iff — Mathlib

English

For any f: β → α, any n ≥ 2, and a ∈ WithBot β, we have ofNat(n) = a.map f iff ∃ x with a = some x and f x = n.

Русский

Для любого f: β → α, n ≥ 2 и a ∈ WithBot β, образ nat(n) равен карте a.map f тогда и только тогда, когда существует x такая, что a = some x и f x = n.

LaTeX

$$$\\forall {f : β \\to α} {n : \\mathbb{N}} [n.AtLeastTwo] {a : \\mathrm{WithBot}\\ β},\\ \\mathrm{instOfNatAtLeastTwo.ofNat}\\ n = (a.map f) \\iff \\exists x, a = \\mathrm{WithBot}.some x ∧ f x = n$$

Lean4

theorem ofNat_eq_map_iff {f : β → α} {n : ℕ} [n.AtLeastTwo] {a : WithBot β} :
    ofNat(n) = a.map f ↔ ∃ x, a = .some x ∧ f x = n :=
  some_eq_map_iff

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