restrictPreimage_injective — Mathlib

English

If f is injective, then the restricted preimage map t.restrictPreimage f is injective.

Русский

Если f инъективна, то ограниченное по предобразу отображение t.restrictPreimage f инъективно.

LaTeX

$$$\text{Injective}(f) \Rightarrow \text{Injective}(t.\restrictPreimage f)$$$

Lean4

theorem restrictPreimage_injective (hf : Injective f) : Injective (t.restrictPreimage f) := fun _ _ e =>
  Subtype.coe_injective <| hf <| Subtype.mk.inj e

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