map_injective — Mathlib

English

If f is injective and respects predicates via h, then the induced map on subtypes is injective.

Русский

Если f инъективно отображает элементы и сохраняет предикаты через h, то полученное отображение на подтипах инъективно.

LaTeX

$$$\forall f,p,q,h,hf:\; (\forall a\, p(a)\rightarrow q(f(a)))\; \&\; Injective f\; \Rightarrow\; Injective (\mathrm{map}\, f\, h)$$$

Lean4

theorem map_injective {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ a, p a → q (f a)) (hf : Injective f) :
    Injective (map f h) :=
  coind_injective _ <| hf.comp coe_injective

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