equiv — Mathlib

English

If a function f is a bijection between sets s ⊆ α and t ⊆ β, then restricting f to s yields an equivalence between the subtypes s and t.

Русский

Если функция f является биекцией между подмножествами s ⊆ α и t ⊆ β, то ограничение f на s дает эквив между подтипами s и t.

LaTeX

$$If h : BijOn f s t, then s ≃ t$$

Lean4

/-- If a function is a bijection between two sets `s` and `t`, then it induces an
equivalence between the types `↥s` and `↥t`. -/
noncomputable def equiv {α : Type*} {β : Type*} {s : Set α} {t : Set β} (f : α → β) (h : BijOn f s t) : s ≃ t :=
  Equiv.ofBijective _ h.bijective

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