left_invariant' — Mathlib

English

If two LeftInvariantDerivation X and Y agree on all test functions, then X = Y.

Русский

Если две левые инвариантные выводимости X и Y совпадают на всех тестовых функциях, то X = Y.

LaTeX

$$Extensionality: (∀ f, X f = Y f) → X = Y$$

Lean4

/-- Premature version of the lemma. Prefer using `left_invariant` instead. -/
theorem left_invariant' : 𝒅ₕ (smoothLeftMul_one I g) (Derivation.evalAt (1 : G) ↑X) = Derivation.evalAt g ↑X :=
  left_invariant'' X g

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