gc_inf_himp — Mathlib

English

The map x ↦ a ∧ x is left adjoint to x ↦ a → x; i.e., Galois connection between ∧ and → with fixed a.

Русский

Связь Гало между ⋀ и ⇨ с фиксированным a: x ↦ a ∧ x и x ↦ a → x образуют пары сопряжённых отображений.

LaTeX

$$$ GaloisConnection (a \wedge \cdot) (a \to \cdot) $$$

Lean4

theorem gc_inf_himp : GaloisConnection (a ⊓ ·) (a ⇨ ·) := fun _ _ ↦ Iff.symm le_himp_iff'

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