bijOn_singleton — Mathlib

English

Let f be a function. The restriction of f to the singleton {a} is a bijection onto the singleton {b} if and only if f(a) = b.

Русский

Пусть f — функция. Ограничение f на единственный элемент {a} является биекцией на {b} тогда и только тогда, когда f(a) = b.

LaTeX

$$$\\text{BijOn}(f,\\{a\\},\\{b\\}) \\quad\\Longleftrightarrow\\quad f(a)=b$$

Lean4

@[simp]
theorem bijOn_singleton : BijOn f { a } { b } ↔ f a = b := by simp [BijOn, eq_comm]

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