inf'_sup_inf' — Mathlib

English

Let α be a distributive lattice. For finite s ⊆ ι, t ⊆ κ and f : ι → α, g : κ → α, one has\n\\[ s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' (hs.product ht) fun i => f i.1 ⊔ g i.2. \\]

Русский

Пусть α распределённая решётка. Тогда\n\\[ s.inf' hs f \\vee t.inf' ht g = (s ×ˢ t).inf' (hs.product ht) (λ i, f i.1 ∨ g i.2). \\]

LaTeX

$$$$ s.inf' hs f \\vee t.inf' ht g = (s \\times\\! t)^{\\inf'} (hs.product ht) (\\lambda i, f(i.1) \\vee g(i.2)). $$$$

Lean4

theorem inf'_sup_inf' (f : ι → α) (g : κ → α) :
    s.inf' hs f ⊔ t.inf' ht g = (s ×ˢ t).inf' (hs.product ht) fun i => f i.1 ⊔ g i.2 :=
  @sup'_inf_sup' αᵒᵈ _ _ _ _ _ hs ht _ _

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