Composition

📁 Source: Mathlib/Topology/OpenPartialHomeomorph/Composition.lean

Statistics

Metric	Count
Definitions `Composition`, `transOpenPartialHomeomorph`, `transPartialHomeomorph`, `trans`, `trans'`	5
Theorems `transOpenPartialHomeomorph_apply`, `transOpenPartialHomeomorph_eq_trans`, `transOpenPartialHomeomorph_source`, `transOpenPartialHomeomorph_symm_apply`, `transOpenPartialHomeomorph_target`, `transOpenPartialHomeomorph_trans`, `transPartialHomeomorph_eq_trans`, `transPartialHomeomorph_trans`, `trans_toOpenPartialHomeomorph`, `trans_toPartialHomeomorph`, `trans_transOpenPartialHomeomorph`, `trans_transPartialHomeomorph`, `trans'`, `coe_trans`, `coe_trans_symm`, `image_trans_source`, `inv_image_trans_target`, `ofSet_trans`, `ofSet_trans'`, `ofSet_trans_ofSet`, `refl_trans`, `restr_symm_trans`, `restr_trans`, `self_trans_symm`, `symm_trans_restr`, `symm_trans_self`, `trans'_apply`, `trans'_source`, `trans'_symm_apply`, `trans'_target`, `trans'_toPartialEquiv`, `trans_apply`, `trans_assoc`, `trans_ofSet`, `trans_of_set'`, `trans_refl`, `trans_source`, `trans_source'`, `trans_source''`, `trans_symm_eq_symm_trans_symm`, `trans_target`, `trans_target'`, `trans_target''`, `trans_toPartialEquiv`	44
Total	49

Homeomorph

Definitions

Name	Category	Theorems
`transOpenPartialHomeomorph` 📖	CompOp	10 math math: `transPartialHomeomorph_trans`, `trans_transPartialHomeomorph`, `transPartialHomeomorph_eq_trans`, `trans_transOpenPartialHomeomorph`, `transOpenPartialHomeomorph_eq_trans`, `transOpenPartialHomeomorph_trans`, `transOpenPartialHomeomorph_target`, `transOpenPartialHomeomorph_symm_apply`, `transOpenPartialHomeomorph_source`, `transOpenPartialHomeomorph_apply`
`transPartialHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`transOpenPartialHomeomorph_apply` 📖	mathematical	—	`OpenPartialHomeomorph.toFun'` `transOpenPartialHomeomorph` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	—
`transOpenPartialHomeomorph_eq_trans` 📖	mathematical	—	`transOpenPartialHomeomorph` `OpenPartialHomeomorph.trans` `toOpenPartialHomeomorph`	—	`OpenPartialHomeomorph.toPartialEquiv_injective` `Equiv.transPartialEquiv_eq_trans`
`transOpenPartialHomeomorph_source` 📖	mathematical	—	`PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `transOpenPartialHomeomorph` `Set.preimage` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	—
`transOpenPartialHomeomorph_symm_apply` 📖	mathematical	—	`OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `transOpenPartialHomeomorph` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`transOpenPartialHomeomorph_target` 📖	mathematical	—	`PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv` `transOpenPartialHomeomorph`	—	—
`transOpenPartialHomeomorph_trans` 📖	mathematical	—	`OpenPartialHomeomorph.trans` `transOpenPartialHomeomorph`	—	`transOpenPartialHomeomorph_eq_trans` `OpenPartialHomeomorph.trans_assoc`
`transPartialHomeomorph_eq_trans` 📖	mathematical	—	`transOpenPartialHomeomorph` `OpenPartialHomeomorph.trans` `toOpenPartialHomeomorph`	—	`transOpenPartialHomeomorph_eq_trans`
`transPartialHomeomorph_trans` 📖	mathematical	—	`OpenPartialHomeomorph.trans` `transOpenPartialHomeomorph`	—	`transOpenPartialHomeomorph_trans`
`trans_toOpenPartialHomeomorph` 📖	mathematical	—	`toOpenPartialHomeomorph` `trans` `OpenPartialHomeomorph.trans`	—	`OpenPartialHomeomorph.toPartialEquiv_injective` `Equiv.trans_toPartialEquiv`
`trans_toPartialHomeomorph` 📖	mathematical	—	`toOpenPartialHomeomorph` `trans` `OpenPartialHomeomorph.trans`	—	`trans_toOpenPartialHomeomorph`
`trans_transOpenPartialHomeomorph` 📖	mathematical	—	`transOpenPartialHomeomorph` `trans`	—	`transOpenPartialHomeomorph_eq_trans` `trans_toOpenPartialHomeomorph` `OpenPartialHomeomorph.trans_assoc`
`trans_transPartialHomeomorph` 📖	mathematical	—	`transOpenPartialHomeomorph` `trans`	—	`trans_transOpenPartialHomeomorph`

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
`trans` 📖	CompOp	65 math math: `trans_apply`, `subtypeRestr_symm_trans_subtypeRestr`, `trans_refl`, `image_trans_source`, `lift_openEmbedding_trans_apply`, `ofSet_trans'`, `Homeomorph.transPartialHomeomorph_trans`, `trans_source'`, `Trivialization.contMDiffOn_symm_trans`, `self_trans_symm`, `restr_trans`, `EqOnSource.trans'`, `FiberBundle.chartedSpace_chartAt`, `trans_source''`, `Homeomorph.transPartialHomeomorph_eq_trans`, `inv_image_trans_target`, `symm_trans_mem_contDiffGroupoid`, `FiberwiseLinear.trans_openPartialHomeomorph_apply`, `FiberwiseLinear.source_trans_PartialHomeomorph`, `lift_openEmbedding_trans`, `StructureGroupoid.compatible_of_mem_maximalAtlas`, `Homeomorph.trans_toPartialHomeomorph`, `trans_transHomeomorph`, `trans_assoc`, `symm_trans_self`, `StructureGroupoid.compatible`, `ext_coord_change_source`, `TangentBundle.chartAt`, `trans_toPartialEquiv`, `ofSet_trans_ofSet`, `IsManifold.compatible_of_mem_maximalAtlas`, `Homeomorph.transOpenPartialHomeomorph_eq_trans`, `trans_ofSet`, `FiberwiseLinear.target_trans_openPartialHomeomorph`, `prod_symm_trans_prod`, `Homeomorph.trans_toOpenPartialHomeomorph`, `trans_source`, `trans_target'`, `StructureGroupoid.trans_restricted`, `symm_trans_restr`, `trans_symm_eq_symm_trans_symm`, `FiberwiseLinear.target_trans_PartialHomeomorph`, `chartAt_comp`, `Homeomorph.transOpenPartialHomeomorph_trans`, `subtypeRestr_def`, `trans_of_set'`, `coe_trans`, `StructureGroupoid.trans`, `Structomorph.mem_groupoid`, `StructureGroupoid.trans'`, `refl_trans`, `coe_trans_symm`, `extend_coord_change_source`, `FiberwiseLinear.trans_PartialHomeomorph_apply`, `prod_trans`, `FiberwiseLinear.source_trans_openPartialHomeomorph`, `trans_target`, `MDifferentiable.trans`, `ofSet_trans`, `transHomeomorph_eq_trans`, `StructureGroupoid.restriction_mem_maximalAtlas_subtype`, `HasGroupoid.compatible`, `trans_target''`, `restr_symm_trans`, `mem_maximalAtlas_iff`
`trans'` 📖	CompOp	5 math math: `trans'_symm_apply`, `trans'_toPartialEquiv`, `trans'_source`, `trans'_target`, `trans'_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_trans` 📖	mathematical	—	`toFun'` `trans`	—	—
`coe_trans_symm` 📖	mathematical	—	`toFun'` `symm` `trans`	—	—
`image_trans_source` 📖	mathematical	—	`Set.image` `toFun'` `PartialEquiv.source` `toPartialEquiv` `trans` `Set` `Set.instInter` `PartialEquiv.target`	—	`PartialEquiv.image_trans_source`
`inv_image_trans_target` 📖	mathematical	—	`Set.image` `toFun'` `symm` `PartialEquiv.target` `toPartialEquiv` `trans` `Set` `Set.instInter` `PartialEquiv.source`	—	`image_trans_source`
`ofSet_trans` 📖	mathematical	`IsOpen`	`trans` `ofSet` `restr`	—	`ext` `IsOpen.interior_eq` `Set.inter_comm`
`ofSet_trans'` 📖	mathematical	`IsOpen`	`trans` `ofSet` `restr` `Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv`	—	`ofSet_trans` `restr_source_inter`
`ofSet_trans_ofSet` 📖	mathematical	`IsOpen`	`trans` `ofSet` `Set` `Set.instInter` `IsOpen.inter`	—	`IsOpen.inter` `trans_ofSet` `ext` `Set.ext` `IsOpen.interior_eq`
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	`toPartialEquiv_injective` `PartialEquiv.refl_trans`
`restr_symm_trans` 📖	mathematical	`IsOpen` `Set.image` `toFun'` `Set` `Set.instHasSubset` `PartialEquiv.source` `toPartialEquiv`	`OpenPartialHomeomorph` `eqOnSourceSetoid` `trans` `symm` `restr`	—	`interior_eq_iff_isOpen` `Set.inter_assoc` `Set.inter_comm` `image_source_inter_eq'` `image_source_eq_target` `Set.image_inter_on` `left_inv`
`restr_trans` 📖	mathematical	—	`trans` `restr`	—	`toPartialEquiv_injective` `PartialEquiv.restr_trans`
`self_trans_symm` 📖	mathematical	—	`OpenPartialHomeomorph` `eqOnSourceSetoid` `trans` `symm` `ofSet` `PartialEquiv.source` `toPartialEquiv` `open_source`	—	`PartialEquiv.self_trans_symm`
`symm_trans_restr` 📖	mathematical	`IsOpen`	`OpenPartialHomeomorph` `eqOnSourceSetoid` `trans` `symm` `restr` `Set` `Set.instInter` `PartialEquiv.target` `toPartialEquiv` `Set.preimage` `toFun'`	—	`image_source_inter_eq'` `isOpen_image_source_inter` `interior_eq_iff_isOpen` `Set.inter_assoc` `Set.inter_comm` `open_target` `interior_inter` `Set.inter_self`
`symm_trans_self` 📖	mathematical	—	`OpenPartialHomeomorph` `eqOnSourceSetoid` `trans` `symm` `ofSet` `PartialEquiv.target` `toPartialEquiv` `open_target`	—	`self_trans_symm`
`trans'_apply` 📖	mathematical	`PartialEquiv.target` `toPartialEquiv` `PartialEquiv.source`	`toFun'` `trans'`	—	—
`trans'_source` 📖	mathematical	`PartialEquiv.target` `toPartialEquiv` `PartialEquiv.source`	`trans'`	—	—
`trans'_symm_apply` 📖	mathematical	`PartialEquiv.target` `toPartialEquiv` `PartialEquiv.source`	`toFun'` `symm` `trans'`	—	—
`trans'_target` 📖	mathematical	`PartialEquiv.target` `toPartialEquiv` `PartialEquiv.source`	`trans'`	—	—
`trans'_toPartialEquiv` 📖	mathematical	`PartialEquiv.target` `toPartialEquiv` `PartialEquiv.source`	`trans'` `PartialEquiv.trans'`	—	—
`trans_apply` 📖	mathematical	—	`toFun'` `trans`	—	—
`trans_assoc` 📖	mathematical	—	`trans`	—	`toPartialEquiv_injective` `PartialEquiv.trans_assoc`
`trans_ofSet` 📖	mathematical	`IsOpen`	`trans` `ofSet` `restr` `Set.preimage` `toFun'`	—	`ext` `trans_source` `restr_source` `ofSet_source` `preimage_interior` `IsOpen.interior_eq`
`trans_of_set'` 📖	mathematical	`IsOpen`	`trans` `ofSet` `restr` `Set` `Set.instInter` `PartialEquiv.source` `toPartialEquiv` `Set.preimage` `toFun'`	—	`trans_ofSet` `restr_source_inter`
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	`toPartialEquiv_injective` `PartialEquiv.trans_refl`
`trans_source` 📖	mathematical	—	`PartialEquiv.source` `toPartialEquiv` `trans` `Set` `Set.instInter` `Set.preimage` `toFun'`	—	`PartialEquiv.trans_source`
`trans_source'` 📖	mathematical	—	`PartialEquiv.source` `toPartialEquiv` `trans` `Set` `Set.instInter` `Set.preimage` `toFun'` `PartialEquiv.target`	—	`PartialEquiv.trans_source'`
`trans_source''` 📖	mathematical	—	`PartialEquiv.source` `toPartialEquiv` `trans` `Set.image` `toFun'` `symm` `Set` `Set.instInter` `PartialEquiv.target`	—	`PartialEquiv.trans_source''`
`trans_symm_eq_symm_trans_symm` 📖	mathematical	—	`symm` `trans`	—	—
`trans_target` 📖	mathematical	—	`PartialEquiv.target` `toPartialEquiv` `trans` `Set` `Set.instInter` `Set.preimage` `toFun'` `symm`	—	—
`trans_target'` 📖	mathematical	—	`PartialEquiv.target` `toPartialEquiv` `trans` `Set` `Set.instInter` `Set.preimage` `toFun'` `symm` `PartialEquiv.source`	—	`trans_source'`
`trans_target''` 📖	mathematical	—	`PartialEquiv.target` `toPartialEquiv` `trans` `Set.image` `toFun'` `Set` `Set.instInter` `PartialEquiv.source`	—	`trans_source''`
`trans_toPartialEquiv` 📖	mathematical	—	`toPartialEquiv` `trans` `PartialEquiv.trans`	—	—

OpenPartialHomeomorph.EqOnSource

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans'` 📖	mathematical	`OpenPartialHomeomorph` `OpenPartialHomeomorph.eqOnSourceSetoid`	`OpenPartialHomeomorph.trans`	—	`PartialEquiv.EqOnSource.trans'`

(root)

Definitions

Name	Category	Theorems
`Composition` 📖	CompData	23 math math: `FormalMultilinearSeries.comp_rightInv_aux1`, `FormalMultilinearSeries.comp_partialSum`, `Composition.reverse_bijective`, `Composition.reverse_surjective`, `composition_card`, `Composition.reverse_involutive`, `FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop`, `FormalMultilinearSeries.compChangeOfVariables_blocksFun`, `FormalMultilinearSeries.compChangeOfVariables_length`, `Composition.cast_heq`, `Composition.sigma_pi_composition_eq_iff`, `FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1`, `Composition.reverse_injective`, `Composition.sigma_eq_iff_blocks_eq`, `Composition.sigma_composition_eq_iff`, `Composition.cast_eq_cast`, `Nat.Partition.ofComposition_surj`, `FormalMultilinearSeries.rightInv_coeff`, `FormalMultilinearSeries.comp_rightInv_aux2`, `FormalMultilinearSeries.mem_compPartialSumTarget_iff`, `FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_atTop`, `FormalMultilinearSeries.comp_summable_nnreal`, `FormalMultilinearSeries.compChangeOfVariables_sum`

---

← Back to Index