map_eq_natCast_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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