Documentation Verification Report

Fibration

📁 Source: Mathlib/Order/UpperLower/Fibration.lean

Statistics

Metric	Count
Definitions `Fibration`, `Fibration`	2
Theorems `image_fibration`, `image_fibration`, `isLowerSet_image`, `isUpperSet_image`, `fibration_iff_image_Ici`, `fibration_iff_image_Iic`, `fibration_iff_isLowerSet_image`, `fibration_iff_isLowerSet_image_Iic`, `fibration_iff_isUpperSet_image`, `fibration_iff_isUpperSet_image_Ici`	10
Total	12

HomotopicalAlgebra

Definitions

Name	Category	Theorems
`Fibration` 📖	CompData	29 math math: `fibration_op_iff`, `instFibrationFstOfIsStableUnderBaseChangeFibrations`, `isFibrant_iff_of_isTerminal`, `instFibrationFstOfIsFibrant`, `instFibrationOppositeOpOfCofibration`, `cofibration_op_iff`, `fibration_iff`, `PathObject.instFibrationP₀`, `instFibrationPCofibrationsTrivialFibrations`, `CofibrantObject.instFibrationPResolutionObj`, `instFibrationOfIsWeakFactorizationSystemCofibrationsTrivialFibrationsOfIsIso`, `Cylinder.IsVeryGood.fibration_π`, `FibrantBrownFactorization.fibration_r`, `instFibrationUnopOfCofibrationOpposite`, `PathObject.instFibrationP₁`, `instFibrationLeftDiscretePUnitOfOver`, `instFibrationPTrivialCofibrationsFibrations`, `fibration_unop_iff`, `mem_trivialFibrations_iff`, `isFibrant_iff`, `cofibration_unop_iff`, `instFibrationSndOfIsFibrant`, `instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1`, `CofibrantObject.HoCat.exists_resolution`, `SSet.modelCategoryQuillen.fibration_iff`, `instFibrationSndOfIsStableUnderBaseChangeFibrations`, `PathObject.IsGood.fibration_p`, `instFibrationCompOfIsStableUnderCompositionFibrations`, `fibrations_over_iff`

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_fibration` 📖	mathematical	`Relation.Fibration` `IsLowerSet`	`Set.image`	—	`Relation.Fibration.isLowerSet_image`

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_fibration` 📖	mathematical	`Relation.Fibration` `IsUpperSet`	`Set.image`	—	`Relation.Fibration.isUpperSet_image`

Relation

Definitions

Name	Category	Theorems
`Fibration` 📖	MathDef	9 math math: `antisymmetrization_fibration`, `fibration_iff_isLowerSet_image`, `fibration_iff_isUpperSet_image`, `DFinsupp.lex_fibration`, `fibration_iff_image_Ici`, `cutExpand_fibration`, `fibration_iff_isLowerSet_image_Iic`, `fibration_iff_image_Iic`, `fibration_iff_isUpperSet_image_Ici`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fibration_iff_image_Ici` 📖	mathematical	`Monotone`	`Fibration` `Preorder.toLE` `Set.image` `Set.Ici`	—	`fibration_iff_image_Iic` `Monotone.dual`
`fibration_iff_image_Iic` 📖	mathematical	`Monotone`	`Fibration` `Preorder.toLE` `Set.image` `Set.Iic`	—	`le_antisymm` `IsLowerSet.Iic_subset` `Fibration.isLowerSet_image` `isLowerSet_Iic` `le_rfl` `fibration_iff_isLowerSet_image_Iic`
`fibration_iff_isLowerSet_image` 📖	mathematical	—	`Fibration` `Preorder.toLE` `IsLowerSet` `Set.image`	—	`Fibration.isLowerSet_image` `fibration_iff_isLowerSet_image_Iic` `isLowerSet_Iic`
`fibration_iff_isLowerSet_image_Iic` 📖	mathematical	—	`Fibration` `Preorder.toLE` `IsLowerSet` `Set.image` `Set.Iic`	—	`IsLowerSet.image_fibration` `isLowerSet_Iic` `le_rfl`
`fibration_iff_isUpperSet_image` 📖	mathematical	—	`Fibration` `Preorder.toLE` `IsUpperSet` `Set.image`	—	`fibration_iff_isLowerSet_image`
`fibration_iff_isUpperSet_image_Ici` 📖	mathematical	—	`Fibration` `Preorder.toLE` `IsUpperSet` `Set.image` `Set.Ici`	—	`fibration_iff_isLowerSet_image_Iic`

Relation.Fibration

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLowerSet_image` 📖	mathematical	`Relation.Fibration` `IsLowerSet`	`Set.image`	—	—
`isUpperSet_image` 📖	mathematical	`Relation.Fibration` `IsUpperSet`	`Set.image`	—	`isLowerSet_image`

---

← Back to Index