comp_ofDual — Mathlib

English

For any f: α → E, and set s, the variation of f after composing with the dual equivalence equals the original variation on s: eVariationOn (f ∘ ofDual) (ofDual⁻¹' s) = eVariationOn f s.

Русский

Для любой функции f: α → E и множества s, вариация после композиции с двойственным отображением равна исходной вариации: eVariationOn (f ∘ ofDual) (ofDual⁻¹' s) = eVariationOn f s.

LaTeX

$$$eVariationOn\\bigl(f \\circ \\mathrm{ofDual}\\bigr)\\bigl(\\mathrm{ofDual}^{-1}'s\\,s\\bigr) = eVariationOn f s$$

Lean4

theorem comp_ofDual (f : α → E) (s : Set α) : eVariationOn (f ∘ ofDual) (ofDual ⁻¹' s) = eVariationOn f s :=
  by
  convert comp_eq_of_antitoneOn f ofDual fun _ _ _ _ => id
  simp only [Equiv.image_preimage]

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