Commit 2023-03-10 06:58 756f1306

View on Github →

feat: port Topology.FiberBundle.Trivialization (#2707)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Bundle.lean

Created Mathlib/Topology/FiberBundle/Trivialization.lean

added theorem Pretrivialization.apply_mk_symm

added theorem Pretrivialization.apply_symm_apply'

added theorem Pretrivialization.apply_symm_apply

added theorem Pretrivialization.coe_coe

added theorem Pretrivialization.coe_coe_fst

added theorem Pretrivialization.coe_fst'

added theorem Pretrivialization.coe_fst

added theorem Pretrivialization.coe_mem_source

added theorem Pretrivialization.coe_symm_of_not_mem

added theorem Pretrivialization.ext'

added theorem Pretrivialization.ext

added theorem Pretrivialization.mem_source

added theorem Pretrivialization.mem_target

added theorem Pretrivialization.mk_mem_target

added theorem Pretrivialization.mk_proj_snd'

added theorem Pretrivialization.mk_proj_snd

added theorem Pretrivialization.mk_symm

added theorem Pretrivialization.preimage_symm_proj_baseSet

added theorem Pretrivialization.preimage_symm_proj_inter

added theorem Pretrivialization.proj_surjOn_baseSet

added theorem Pretrivialization.proj_symm_apply'

added theorem Pretrivialization.proj_symm_apply

added def Pretrivialization.setSymm

added theorem Pretrivialization.symm_apply

added theorem Pretrivialization.symm_apply_apply

added theorem Pretrivialization.symm_apply_apply_mk

added theorem Pretrivialization.symm_apply_mk_proj

added theorem Pretrivialization.symm_apply_of_not_mem

added theorem Pretrivialization.symm_coe_proj

added theorem Pretrivialization.symm_proj_apply

added theorem Pretrivialization.symm_trans_source_eq

added theorem Pretrivialization.symm_trans_symm

added theorem Pretrivialization.symm_trans_target_eq

added theorem Pretrivialization.target_inter_preimage_symm_source_eq

added def Pretrivialization.toFun'

added theorem Pretrivialization.toLocalEquiv_injective

added theorem Pretrivialization.trans_source

added structure Pretrivialization

added theorem Trivialization.apply_mk_symm

added theorem Trivialization.apply_symm_apply'

added theorem Trivialization.apply_symm_apply

added theorem Trivialization.coe_coe

added theorem Trivialization.coe_coe_fst

added theorem Trivialization.coe_fst'

added theorem Trivialization.coe_fst

added theorem Trivialization.coe_fst_eventuallyEq_proj'

added theorem Trivialization.coe_fst_eventuallyEq_proj

added theorem Trivialization.coe_mem_source

added theorem Trivialization.coe_mk

added theorem Trivialization.continuousAt_of_comp_left

added theorem Trivialization.continuousAt_of_comp_right

added theorem Trivialization.continuousAt_proj

added theorem Trivialization.continuousOn_symm

added theorem Trivialization.continuous_coordChange

added def Trivialization.coordChange

added theorem Trivialization.coordChangeHomeomorph_coe

added theorem Trivialization.coordChange_apply_snd

added theorem Trivialization.coordChange_coordChange

added theorem Trivialization.coordChange_same

added theorem Trivialization.coordChange_same_apply

added theorem Trivialization.ext'

added theorem Trivialization.frontier_preimage

added theorem Trivialization.image_preimage_eq_prod_univ

added theorem Trivialization.isImage_preimage_prod

added theorem Trivialization.map_proj_nhds

added theorem Trivialization.map_target

added theorem Trivialization.mem_source

added theorem Trivialization.mem_target

added theorem Trivialization.mk_coordChange

added theorem Trivialization.mk_mem_target

added theorem Trivialization.mk_proj_snd'

added theorem Trivialization.mk_proj_snd

added theorem Trivialization.mk_symm

added theorem Trivialization.open_target'

added def Trivialization.preimageHomeomorph

added theorem Trivialization.preimageHomeomorph_apply

added theorem Trivialization.preimageHomeomorph_symm_apply

added def Trivialization.preimageSingletonHomeomorph

added theorem Trivialization.preimageSingletonHomeomorph_apply

added theorem Trivialization.preimageSingletonHomeomorph_symm_apply

added theorem Trivialization.preimage_subset_source

added theorem Trivialization.proj_surjOn_baseSet

added theorem Trivialization.proj_symm_apply'

added theorem Trivialization.proj_symm_apply

added def Trivialization.sourceHomeomorphBaseSetProd

added theorem Trivialization.sourceHomeomorphBaseSetProd_apply

added theorem Trivialization.sourceHomeomorphBaseSetProd_symm_apply

added theorem Trivialization.source_inter_preimage_target_inter

added theorem Trivialization.symm_apply

added theorem Trivialization.symm_apply_apply

added theorem Trivialization.symm_apply_apply_mk

added theorem Trivialization.symm_apply_mk_proj

added theorem Trivialization.symm_apply_of_not_mem

added theorem Trivialization.symm_coe_proj

added theorem Trivialization.symm_proj_apply

added theorem Trivialization.symm_trans_source_eq

added theorem Trivialization.symm_trans_target_eq

added def Trivialization.toFun'

added def Trivialization.toPretrivialization

added theorem Trivialization.toPretrivialization_injective

added def Trivialization.transFiberHomeomorph

added theorem Trivialization.transFiberHomeomorph_apply

added structure Trivialization