iff_map_le_isomorphisms — Mathlib

English

W.IsInvertedBy F iff W.map F ≤ isomorphisms D; equivalence between inverting with respect to F and a map-closure condition.

Русский

W разворачивается по F тогда и только тогда, когда W.map F ≤ isomorphisms D; эквивалентность между инверсией по F и условием ограничений отображения.

LaTeX

$$$ W.IsInvertedBy F \iff W.map F \leq \text{isomorphisms } D $$$

Lean4

theorem iff_map_le_isomorphisms (W : MorphismProperty C) (F : C ⥤ D) : W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D := by
  rw [iff_le_inverseImage_isomorphisms, map_le_iff]

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