isLocallyInjective_whisker_iff — Mathlib

English

IsLocallyInjective J (whiskerLeft H.op f) holds iff IsLocallyInjective K f, under cover-preserving adjunctions.

Русский

Локальная инъективность через whiskerLeft сопряжения сохраняется взаимно однозначно.

LaTeX

$$$IsLocallyInjective J (H.op.whiskerLeft f) \iff IsLocallyInjective K f$$$

Lean4

theorem isLocallyInjective_whisker_iff (hH : CoverPreserving J K H) [H.IsCocontinuous J K] [H.IsCoverDense K] :
    IsLocallyInjective J (whiskerLeft H.op f) ↔ IsLocallyInjective K f :=
  ⟨fun _ ↦ isLocallyInjective_of_whisker J K H f hH, fun _ ↦ isLocallyInjective_whisker J K H f⟩

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