sup'_congr — Mathlib

English

If s = t and f agrees with g on s, then s.sup' H f = t.sup' (h1 ▸ H) g.

Русский

Если множества совпадают и функции согласованы на s, то sup' по f равно sup' по g на соответствующей подстановке.

LaTeX

$$$s = t \Rightarrow (\forall x \in s, f x = g x) \Rightarrow s.sup' H f = t.sup' (h_1 \▸ H) g$$$

Lean4

@[congr]
theorem sup'_congr {t : Finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) :
    s.sup' H f = t.sup' (h₁ ▸ H) g := by
  subst s
  refine eq_of_forall_ge_iff fun c => ?_
  simp +contextual only [sup'_le_iff, h₂]

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