sInf_image2_eq_sInf_sInf — Mathlib

English

If h1,h2 provide the appropriate GC's for l1, l2 with swap and ofDual, then sInf(image2 u s t) = u(sInf s)(sInf t).

Русский

Если заданы соответствующие связи Галуа для l1, l2, то sInf(image2 u s t) = u(sInf s)(sInf t).

LaTeX

$$$$ sInf(image2\\ u\\ s\\ t) = u(sInf\\ s)(sInf\\ t). $$$$

Lean4

theorem sInf_image2_eq_sInf_sInf (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sInf s) (sInf t) := by
  simp_rw [sInf_image2, ← (h₂ _).u_sInf, ← (h₁ _).u_sInf]

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