FrameOrientationContinuity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous frame curves stay in the same orientation component.

theorem OAI.PositiveEinsteinFour.Geometry.FrameOrientation.mem_iff_of_continuous_curve line 20
Source documentation
Orientation membership is constant along a continuous real frame curve.
```
theorem FrameOrientation.mem_iff_of_continuous_curve (o : FrameOrientation g)
    (γ : ℝ → FrameBundle g) (hγ : Continuous γ) (s t : ℝ) :
    γ s ∈ o.positive ↔ γ t ∈ o.positive := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameOrientation, OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.FrameFlow.orientation_preserving line 38
Source documentation
A continuous frame flow initialized at the identity preserves each orientation component, independently of measure preservation.
```
theorem FrameFlow.orientation_preserving {μ : Measure (FrameBundle g)}
    (φ : FrameFlow g μ) (hzero : ∀ e, φ.map 0 e = e) (o : FrameOrientation g)
    (t : ℝ) (e : FrameBundle g) :
    φ.map t e ∈ o.positive ↔ e ∈ o.positive := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.FrameOrientation