Plane linear action joint continuous

Proved

BirkhoffGlobalSection.plane_linear_action_joint_continuous

by Mazecto · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometryreal-analysis

A time-indexed real-linear plane action whose value on each fixed input vector is continuous in time has jointly continuous evaluation in time and input.

All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.

Preamble

import Theorems.Thm_BirkhoffGlobalSection_contact_winding_interval_bundle

open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology

set_option maxHeartbeats 800000
open BirkhoffGlobalSection Set Filter Topology
open scoped ContDiff Topology
set_option linter.unusedVariables false


set_option autoImplicit false
set_option maxHeartbeats 800000

Formal statement

theorem BirkhoffGlobalSection.plane_linear_action_joint_continuous :
∀ (A : ℝ → Plane → Plane)
    (hlin : ∀ t (p r : Plane) (a b : ℝ), A t (a • p + b • r) = a • A t p + b • A t r)
    (hcont : ∀ p, Continuous (fun t => A t p)),
    Continuous (fun x : ℝ × Plane => A x.1 x.2) := by sorry

Source

Independent extraction of component 7 of the Proved theorem BirkhoffGlobalSection.contact_winding_interval_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_contact_winding_interval_bundle.lean. Exact original component retained.

View graph