sup_congr — Mathlib

English

If two finite sets are equal and the function values agree on the second set, then their suprema coincide: s1 = s2 and f ≡ g on s2 imply s1.sup f = s2.sup g.

Русский

Если два множества равны и значения функции совпадают на втором множестве, то их верхние грани совпадают.

LaTeX

$$$ (s_1 = s_2) \\Rightarrow (\\forall a \\in s_2, f a = g a) \\Rightarrow s_1.sup f = s_2.sup g $$$

Lean4

theorem sup_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) : s₁.sup f = s₂.sup g :=
  by
  subst hs
  exact Finset.fold_congr hfg

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