monotone_intro — Mathlib

English

If u is monotone, l is monotone, and hul and hlu hold (i.e., a ≤ u(l a) and l(u a) ≤ a for all a), then l and u form a Galois connection: ∀ a,b, l a ≤ b ↔ a ≤ u b.

Русский

Если u монотонна, l монотонна, и hul, hlu выполняются (то есть a ≤ u(l a) и l(u a) ≤ a для всех a), тогда l и u образуют связь Галуа: ∀ a,b, l a ≤ b ↔ a ≤ u b.

LaTeX

$$$\forall a,b:\ l a \le b \iff a \le u b$$$

Lean4

theorem monotone_intro (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a)) (hlu : ∀ a, l (u a) ≤ a) :
    GaloisConnection l u := fun _ _ => ⟨fun h => (hul _).trans (hu h), fun h => (hl h).trans (hlu _)⟩

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