gc_llp_rlp — Mathlib

English

There is a Galois connection between llp and rlp under dualization, expressing a duality between left and right lifting properties.

Русский

Существует связь Гало между LLP и RLP под двойственным отображением, выражающая дуальность между левыми и правыми свойствами заполнения.

LaTeX

$$$\mathrm{GaloisConnection}\left(\mathrm{OrderDual.toDual} \circ \mathrm{llp},\; \mathrm{rlp} \circ \mathrm{OrderDual.ofDual}\right)$$$

Lean4

theorem gc_llp_rlp : GaloisConnection (OrderDual.toDual (α := MorphismProperty C) ∘ llp) (rlp ∘ OrderDual.ofDual) :=
  fun _ _ ↦ le_llp_iff_le_rlp _ _

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