inf'_congr — Mathlib

English

If h1 expresses equality of two finite sets and h2 states pointwise equality of functions on the first set, then the infimums coincide.

Русский

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

LaTeX

$$$\\text{Inf'_congr}: s = t \\Rightarrow (\\forall x \\in s, f x = g x) \\Rightarrow s.inf' H f = t.inf' H g$$$

Lean4

@[congr]
theorem inf'_congr {t : Finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) :
    s.inf' H f = t.inf' (h₁ ▸ H) g :=
  sup'_congr (α := αᵒᵈ) H h₁ h₂

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