subset_left — Mathlib

English

If h is a bijection on s to t, then restricting to any r ⊆ s produces a bijection on r to its image.

Русский

Если h — биекция на s→t, то ограничение на любой r ⊆ s даёт биекцию на r к его образу.

LaTeX

$$$\\text{BijOn}(f,s,t) \\land r \\subseteq s \\Rightarrow \\text{BijOn}(f,r, f''r)$$$

Lean4

theorem subset_left {r : Set α} (hf : BijOn f s t) (hrs : r ⊆ s) : BijOn f r (f '' r) :=
  (hf.injOn.mono hrs).bijOn_image

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