map_eq_ofNat_iff — Mathlib

English

For any f: β → α, any n ≥ 2, and any a ∈ WithBot β, a.map f = ofNat(n) if and only if there exists x with a = some x and f x = n.

Русский

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

LaTeX

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

Lean4

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

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