CencovPetz.ContinuousExtension #
Reusable “extend equality from a dense set” lemmas for functions on the finite open simplex.
This is used in the last step of the finite Čencov/Chentsov argument: once an identity is shown on a dense family of rational/common-denominator points, continuity hypotheses allow extending the identity to all simplex points.
Main result #
theorem
LeanPool.CencovPetz.eq_of_eqOn_dense₂
{α : Type u}
[Fintype α]
{s : Set (Simplex α)}
(hs : Dense s)
{f g : Simplex α → ↥(tangentSpace α) → ↥(tangentSpace α) → ℝ}
(hf : ∀ (u v : ↥(tangentSpace α)), Continuous fun (p : Simplex α) => f p u v)
(hg : ∀ (u v : ↥(tangentSpace α)), Continuous fun (p : Simplex α) => g p u v)
(hfg : ∀ p ∈ s, ∀ (u v : ↥(tangentSpace α)), f p u v = g p u v)
(p : Simplex α)
(u v : ↥(tangentSpace α))
: