bijective — Mathlib

English

Repeating a subsingleton-based bijection principle for clarity in proofs.

Русский

Повторение принципа биекции на основе подселективности для ясности доказательств.

LaTeX

$$$[Subsingleton] (f s t) : BijOn f s t$$$

Lean4

theorem bijective (h : BijOn f s t) : Bijective (h.mapsTo.restrict f s t) :=
  ⟨fun x y h' => Subtype.ext <| h.injOn x.2 y.2 <| Subtype.ext_iff.1 h', fun ⟨_, hy⟩ =>
    let ⟨x, hx, hxy⟩ := h.surjOn hy
    ⟨⟨x, hx⟩, Subtype.eq hxy⟩⟩

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