sup'_comm — Mathlib

English

The order of taking supremums over two Finsets is interchangeable: a two-variable supremum is symmetric in its arguments.

Русский

Порядок взятия supremum по двум конечным множествам взаимно соответствует: дихотомический максимум симметричен относительно аргументов.

LaTeX

$$$(s \sup' hs (\lambda b. t.sup' ht (f\, b))) = (t.sup' ht (\lambda c. s.sup' hs (\lambda b. f\, b\, c)))$$$

Lean4

protected theorem sup'_comm {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β → γ → α) :
    (s.sup' hs fun b => t.sup' ht (f b)) = t.sup' ht fun c => s.sup' hs fun b => f b c :=
  eq_of_forall_ge_iff fun a => by simpa using forall₂_swap

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