bijective — Mathlib

English

If A and B are types with a unique element, then any function f: A → B is bijective.

Русский

Если A и B — типы, имеющие по одному элементу, то любая функция f: A → B биективна.

LaTeX

$$$\\\\forall A B \\\\,[\\\\operatorname{Unique} A] \\\\,[\\\\operatorname{Unique} B] \\\\{f : A \\\\to B\\\\},\\\\;\\\\operatorname{Bijective}(f)$$$

Lean4

theorem bijective {A B} [Unique A] [Unique B] {f : A → B} : Function.Bijective f :=
  by
  rw [Function.bijective_iff_has_inverse]
  refine ⟨default, ?_, ?_⟩ <;> intro x <;> simp

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