extend_congr — Mathlib

English

If the predicates P sa and Pb sb are equivalent and the corresponding values match, then the extensions agree: extend m sa = extend mb sb.

Русский

Если предикаты P sa и Pb sb эквивалентны и соответствующие значения совпадают, то расширения совпадают: extend m sa = extend mb sb.

LaTeX

$$If Iff (P sa) (Pb sb) and ∀ ha hb, m sa ha = mb sb hb, then \\mathrm{extend} m sa = \\mathrm{extend} mb sb$$

Lean4

theorem extend_congr {β : Type*} {Pb : β → Prop} {mb : ∀ s : β, Pb s → ℝ≥0∞} {sa : α} {sb : β} (hP : P sa ↔ Pb sb)
    (hm : ∀ (ha : P sa) (hb : Pb sb), m sa ha = mb sb hb) : extend m sa = extend mb sb :=
  iInf_congr_Prop hP fun _h => hm _ _

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