mono_liftExtend_f_iff — Mathlib

English

Let e, φ, hφ be as above. For all i′, i with hi: e.f i = i′, the morphism (e.liftExtend φ hφ).f i′ is mono iff φ.f i is mono.

Русский

Пусть e, φ, hφ как выше. Для всех i′, i с hi: e.f i = i′, отображение (e.liftExtend φ hφ).f i′ линеарно монотонно эквивалентно φ.f i.

LaTeX

$$$$ \forall i\, \forall i'\, (hi : e.f i = i'): \quad Mono\big((e.liftExtend φ hφ).f i'\big) \iff Mono(φ.f i) $$$$

Lean4

theorem mono_liftExtend_f_iff (hi : e.f i = i') : Mono ((e.liftExtend φ hφ).f i') ↔ Mono (φ.f i) :=
  (MorphismProperty.monomorphisms C).arrow_mk_iso_iff (e.liftExtendfArrowIso φ hφ hi)

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