coind_injective — Mathlib

English

If h ensures p after applying f and f is injective, then the coind f h map is injective.

Русский

Если h обеспечивает свойство p после применения f, и f инъективен, то отображение coind f h инъективно.

LaTeX

$$$\\text{Injective}(\\mathrm{Subtype}.coind f h)$$$

Lean4

theorem coind_injective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Injective f) :
    Injective (coind f h) := fun x y hxy ↦ hf <| by apply congr_arg Subtype.val hxy

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