gc_leftDual_rightDual — Mathlib

English

The pair of maps toDual ∘ leftDual and rightDual ∘ ofDual forms a Galois connection.

Русский

Пара отображений toDual ∘ leftDual и rightDual ∘ ofDual образует гамосовую связь.

LaTeX

$$$\text{GaloisConnection}(\mathrm{toDual} \circ R.\mathrm{leftDual},\ R.\mathrm{rightDual} \circ \mathrm{ofDual}).$$$

Lean4

/-- The pair of functions `toDual ∘ leftDual` and `rightDual ∘ ofDual` forms a Galois connection. -/
theorem gc_leftDual_rightDual : GaloisConnection (toDual ∘ R.leftDual) (R.rightDual ∘ ofDual) := fun _ _ ↦
  ⟨fun h _ ha _ hb ↦ h (by simpa) ha, fun h _ hb _ ha ↦ h (by simpa) hb⟩

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