gc_upperPolar_lowerPolar — Mathlib

English

The pair upperPolar and lowerPolar forms a Galois connection under the appropriate dualities.

Русский

Пара upperPolar и lowerPolar образуют связь Галуа при соответствующих двойственностях.

LaTeX

$$$\mathrm{GaloisConnection}(\mathrm{toDual} \circ \mathrm{upperPolar}(r), \mathrm{lowerPolar}(r) \circ \mathrm{ofDual})$$$

Lean4

theorem gc_upperPolar_lowerPolar : GaloisConnection (toDual ∘ upperPolar r) (lowerPolar r ∘ ofDual) := fun _ _ =>
  subset_upperPolar_iff_subset_lowerPolar

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