sup_sup — Mathlib

English

For any s, the supremum distributes over the pointwise join: s.sup (f ⊔ g) = s.sup f ⊔ s.sup g.

Русский

Для любой множества верхняя грань распределяется через точечное объединение: s.sup (f ⊔ g) = s.sup f ⊔ s.sup g.

LaTeX

$$$ s.sup (f \\;\\hbox{⊔}\\; g) = s.sup f \\;\\sqcup\\; s.sup g $$$

Lean4

theorem sup_sup : s.sup (f ⊔ g) = s.sup f ⊔ s.sup g := by
  induction s using Finset.cons_induction with
  | empty => rw [sup_empty, sup_empty, sup_empty, bot_sup_eq]
  | cons _ _ _ ih =>
    rw [sup_cons, sup_cons, sup_cons, ih]
    exact sup_sup_sup_comm _ _ _ _

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