Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-28 13:54 b160ac8d

View on Github →

chore(topology/topological_fiber_bundle): reorganizing the code (#7989) Mainly redesigning the simp strategy.

Estimated changes

Modified src/data/equiv/local_equiv.lean

added theorem local_equiv.source_inter_preimage_target_inter

Modified src/data/set/basic.lean

modified theorem set.preimage_const_of_mem

modified theorem set.preimage_const_of_not_mem

Modified src/geometry/manifold/basic_smooth_bundle.lean

Modified src/topology/constructions.lean

added theorem continuous.prod.mk

Modified src/topology/continuous_on.lean

added theorem continuous_on.is_open_preimage

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.source_inter_preimage_target_inter

Modified src/topology/order.lean

added theorem is_open_induced_iff'

added theorem le_induced_generate_from

Modified src/topology/topological_fiber_bundle.lean

added theorem bundle.coe_fst

added theorem bundle.coe_snd_map_apply

added theorem bundle.coe_snd_map_smul

added def bundle.total_space_mk

added theorem topological_fiber_bundle_core.base_set_at

added theorem topological_fiber_bundle_core.continuous_total_space_mk

modified theorem topological_fiber_bundle_core.local_triv'_apply

added theorem topological_fiber_bundle_core.local_triv'_coe

added theorem topological_fiber_bundle_core.local_triv'_source

modified theorem topological_fiber_bundle_core.local_triv'_symm_apply

added theorem topological_fiber_bundle_core.local_triv'_target

modified theorem topological_fiber_bundle_core.local_triv_apply

deleted def topological_fiber_bundle_core.local_triv_at

added theorem topological_fiber_bundle_core.local_triv_at_apply

modified def topological_fiber_bundle_core.local_triv_at_ext

added theorem topological_fiber_bundle_core.local_triv_at_ext_def

deleted theorem topological_fiber_bundle_core.local_triv_at_ext_to_local_homeomorph

deleted theorem topological_fiber_bundle_core.local_triv_at_fst

deleted theorem topological_fiber_bundle_core.local_triv_at_symm_fst

added theorem topological_fiber_bundle_core.local_triv_coe

added theorem topological_fiber_bundle_core.local_triv_ext_apply

added theorem topological_fiber_bundle_core.local_triv_ext_symm_apply

added theorem topological_fiber_bundle_core.local_triv_ext_symm_fst

added theorem topological_fiber_bundle_core.local_triv_source

added theorem topological_fiber_bundle_core.local_triv_symm

modified theorem topological_fiber_bundle_core.local_triv_symm_fst

added theorem topological_fiber_bundle_core.local_triv_target

modified theorem topological_fiber_bundle_core.mem_local_triv'_source

modified theorem topological_fiber_bundle_core.mem_local_triv'_target

added theorem topological_fiber_bundle_core.mem_local_triv_at_ext_base_set

deleted theorem topological_fiber_bundle_core.mem_local_triv_at_source

added theorem topological_fiber_bundle_core.mem_local_triv_ext_source

added theorem topological_fiber_bundle_core.mem_local_triv_ext_target

modified theorem topological_fiber_bundle_core.mem_local_triv_source

modified theorem topological_fiber_bundle_core.mem_local_triv_target

Modified src/topology/vector_bundle.lean

added theorem topological_vector_bundle.trivialization.coe_coe

added theorem topological_vector_bundle.trivialization.coe_fst