DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Move Lemmas

Browse source
This commit is contained in:
jstoobysmith 2024-11-10 07:00:48 +00:00
parent b0c5ed894f
commit a9143f79b6
2 changed files with 18 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

13
HepLean/Lorentz/RealVector/Basic.lean
View file

@ -33,17 +33,6 @@ def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
instance : TopologicalSpace (Contr d) := TopologicalSpace.induced
ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced
ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
lemma toFin1dℝEquiv_isInducing : IsInducing (@ContrMod.toFin1dℝEquiv d) := by
exact { eq_induced := rfl }
lemma toFin1dℝEquiv_symm_isInducing : IsInducing ((@ContrMod.toFin1dℝEquiv d).symm) := by
let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
toFin1dℝEquiv_isInducing
exact Homeomorph.isInducing x.symm
lemma continuous_contr {T : Type} [TopologicalSpace T] (f : T → Contr d)
(h : Continuous (fun i => (f i).toFin1dℝ)) : Continuous f := by
exact continuous_induced_rng.mpr h
@ -51,7 +40,7 @@ lemma continuous_contr {T : Type} [TopologicalSpace T] (f : T → Contr d)
lemma contr_continuous {T : Type} [TopologicalSpace T] (f : Contr d → T)
(h : Continuous (f ∘ (@ContrMod.toFin1dℝEquiv d).symm)) : Continuous f := by
let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
toFin1dℝEquiv_isInducing
ContrMod.toFin1dℝEquiv_isInducing
rw [← Homeomorph.comp_continuous_iff' x.symm]
exact h

17
HepLean/Lorentz/RealVector/Modules.lean
View file

@ -274,6 +274,23 @@ lemma toSelfAdjoint_symm_basis (i : Fin 1 ⊕ Fin 3) :
refine (LinearEquiv.symm_apply_eq toSelfAdjoint).mpr ?_
rw [toSelfAdjoint_stdBasis]
/-!
## Topology
-/
instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced
ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
lemma toFin1dℝEquiv_isInducing : IsInducing (@ContrMod.toFin1dℝEquiv d) := by
exact { eq_induced := rfl }
lemma toFin1dℝEquiv_symm_isInducing : IsInducing ((@ContrMod.toFin1dℝEquiv d).symm) := by
let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
toFin1dℝEquiv_isInducing
exact Homeomorph.isInducing x.symm
end ContrMod
/-- The module for covariant (up-index) complex Lorentz vectors. -/