natCast_eq_map_iff — Mathlib

English

For any f: β → α, any n ∈ ℕ, and a ∈ WithBot β, n.cast = a.map f iff ∃ x with a = some x and f x = n.cast.

Русский

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

LaTeX

$$$\\forall {f : β \\to α} {n : \\mathbb{N}} {a : \\mathrm{WithBot}\\ β},\\ n.cast = a.map f \\iff \\exists x, a = \\mathrm{WithBot}.some x ∧ f x = n.cast$$

Lean4

theorem natCast_eq_map_iff {f : β → α} {n : ℕ} {a : WithBot β} : n = a.map f ↔ ∃ x, a = .some x ∧ f x = n :=
  some_eq_map_iff

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