Commit 2023-03-22 01:31 33c3899f

View on Github →

feat: port Topology.FiberBundle.Basic (#2862)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.map_comap_setCoe_val

Modified Mathlib/Topology/Constructions.lean

added theorem embedding_prod_mk

Created Mathlib/Topology/FiberBundle/Basic.lean

added theorem FiberBundle.continuous_proj

added theorem FiberBundle.continuous_totalSpaceMk

added theorem FiberBundle.exists_trivialization_Icc_subset

added theorem FiberBundle.isOpenMap_proj

added theorem FiberBundle.map_proj_nhds

added theorem FiberBundle.mem_baseSet_trivializationAt

added theorem FiberBundle.quotientMap_proj

added theorem FiberBundle.surjective_proj

added theorem FiberBundle.totalSpaceMk_closedEmbedding

added theorem FiberBundle.totalSpaceMk_embedding

added theorem FiberBundle.totalSpaceMk_inducing

added theorem FiberBundle.trivialization_mem_atlas

added def FiberBundleCore.Base

added def FiberBundleCore.Fiber

added def FiberBundleCore.Index

added def FiberBundleCore.TotalSpace

added theorem FiberBundleCore.baseSet_at

added theorem FiberBundleCore.continuous_const_section

added theorem FiberBundleCore.continuous_totalSpaceMk

added def FiberBundleCore.localTriv

added def FiberBundleCore.localTrivAsLocalEquiv

added theorem FiberBundleCore.localTrivAsLocalEquiv_apply

added theorem FiberBundleCore.localTrivAsLocalEquiv_coe

added theorem FiberBundleCore.localTrivAsLocalEquiv_source

added theorem FiberBundleCore.localTrivAsLocalEquiv_symm

added theorem FiberBundleCore.localTrivAsLocalEquiv_target

added theorem FiberBundleCore.localTrivAsLocalEquiv_trans

added def FiberBundleCore.localTrivAt

added theorem FiberBundleCore.localTrivAt_apply

added theorem FiberBundleCore.localTrivAt_apply_mk

added theorem FiberBundleCore.localTrivAt_def

added theorem FiberBundleCore.localTrivAt_snd

added theorem FiberBundleCore.localTriv_apply

added theorem FiberBundleCore.localTriv_symm_apply

added theorem FiberBundleCore.mem_localTrivAsLocalEquiv_source

added theorem FiberBundleCore.mem_localTrivAsLocalEquiv_target

added theorem FiberBundleCore.mem_localTrivAt_baseSet

added theorem FiberBundleCore.mem_localTrivAt_source

added theorem FiberBundleCore.mem_localTrivAt_target

added theorem FiberBundleCore.mem_localTriv_source

added theorem FiberBundleCore.mem_localTriv_target

added theorem FiberBundleCore.mem_source_at

added theorem FiberBundleCore.mem_trivChange_source

added theorem FiberBundleCore.open_source'

added def FiberBundleCore.proj

added def FiberBundleCore.trivChange

added structure FiberBundleCore

added theorem FiberPrebundle.continuousOn_of_comp_right

added theorem FiberPrebundle.continuous_proj

added theorem FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas

added theorem FiberPrebundle.continuous_totalSpaceMk

added def FiberPrebundle.fiberTopology

added theorem FiberPrebundle.inducing_totalSpaceMk

added theorem FiberPrebundle.isOpen_source

added theorem FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter

added theorem FiberPrebundle.mem_pretrivializationAt_source

added def FiberPrebundle.toFiberBundle

added theorem FiberPrebundle.totalSpaceMk_preimage_source

added def FiberPrebundle.totalSpaceTopology

added def FiberPrebundle.trivializationOfMemPretrivializationAtlas

added structure FiberPrebundle

Modified Mathlib/Topology/LocalHomeomorph.lean

added theorem LocalHomeomorph.nhds_eq_comap_inf_principal