csInf_image2_eq_csInf_csInf — Mathlib

English

A well-founded linear order with a bottom element yields a conditional complete lattice with a bottom.

Русский

Упорядочение с хорошей фундаментальностью и нулём (самой нижней точкой) образует условно полноупорядоченную решётку с нулём снизу.

LaTeX

$$$\text{WellFoundedLT}.conditionnallyCompleteLinearOrderBot (\alpha)$$$

Lean4

theorem csInf_image2_eq_csInf_csInf (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) :
    s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sInf s) (sInf t) :=
  csSup_image2_eq_csSup_csSup (α := αᵒᵈ) (β := βᵒᵈ) (γ := γᵒᵈ) (u₁ := l₁) (u₂ := l₂) (fun _ => (h₁ _).dual) fun _ =>
    (h₂ _).dual

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