Documentation Verification Report

Constructions

📁 Source: Mathlib/Topology/Bornology/Constructions.lean

Statistics

Metric	Count
Definitions `induced`, `instBornology`, `instBornology`, `instBornologyAdditive`, `instBornologyMultiplicative`, `instBornologyOrderDual`, `instBornologySubtype`	7
Theorems `boundedSpace_subtype`, `boundedSpace_val`, `fst_of_prod`, `image_eval`, `image_fst`, `image_snd`, `pi`, `prod`, `snd_of_prod`, `cobounded_pi`, `cobounded_prod`, `forall_isBounded_image_eval_iff`, `isBounded_image_fst_and_snd`, `isBounded_image_subtype_val`, `isBounded_induced`, `isBounded_pi`, `isBounded_pi_of_nonempty`, `isBounded_prod`, `isBounded_prod_of_nonempty`, `isBounded_prod_self`, `boundedSpace_induced_iff`, `boundedSpace_subtype_iff`, `boundedSpace_val_set_iff`, `instBoundedSpaceAdditive`, `instBoundedSpaceForall`, `instBoundedSpaceMultiplicative`, `instBoundedSpaceOrderDual`, `instBoundedSpaceProd`, `instBoundedSpaceSubtype`	29
Total	36

Bornology

Definitions

Name	Category	Theorems
`induced` 📖	CompOp	5 math math: `bornology_eq_of_bilipschitz`, `isBounded_induced`, `Unitization.cobounded_eq_aux`, `isBounded_iff_of_bilipschitz`, `boundedSpace_induced_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cobounded_pi` 📖	mathematical	—	`cobounded` `Pi.instBornology` `Filter.coprodᵢ`	—	—
`cobounded_prod` 📖	mathematical	—	`cobounded` `Prod.instBornology` `Filter.coprod`	—	—
`forall_isBounded_image_eval_iff` 📖	mathematical	—	`IsBounded` `Set.image` `Function.eval` `Pi.instBornology`	—	`Filter.compl_mem_coprodᵢ`
`isBounded_image_fst_and_snd` 📖	mathematical	—	`IsBounded` `Set.image` `Prod.instBornology`	—	`Filter.compl_mem_coprod`
`isBounded_image_subtype_val` 📖	mathematical	—	`IsBounded` `Set.image` `instBornologySubtype`	—	`isBounded_induced`
`isBounded_induced` 📖	mathematical	—	`IsBounded` `induced` `Set.image`	—	`Filter.compl_mem_comap`
`isBounded_pi` 📖	mathematical	—	`IsBounded` `Pi.instBornology` `Set.pi` `Set.univ` `Set` `Set.instEmptyCollection`	—	`Set.univ_pi_eq_empty_iff` `isBounded_pi_of_nonempty`
`isBounded_pi_of_nonempty` 📖	mathematical	`Set.Nonempty` `Set.pi` `Set.univ`	`IsBounded` `Pi.instBornology`	—	`forall_isBounded_image_eval_iff` `Set.eval_image_univ_pi` `IsBounded.pi`
`isBounded_prod` 📖	mathematical	—	`IsBounded` `Prod.instBornology` `SProd.sprod` `Set` `Set.instSProd` `Set.instEmptyCollection`	—	`Set.eq_empty_or_nonempty` `Set.empty_prod` `Set.prod_empty` `isBounded_prod_of_nonempty` `Set.Nonempty.prod` `Set.Nonempty.ne_empty`
`isBounded_prod_of_nonempty` 📖	mathematical	`Set.Nonempty` `SProd.sprod` `Set` `Set.instSProd`	`IsBounded` `Prod.instBornology`	—	`IsBounded.fst_of_prod` `Set.Nonempty.snd` `IsBounded.snd_of_prod` `Set.Nonempty.fst` `IsBounded.prod`
`isBounded_prod_self` 📖	mathematical	—	`IsBounded` `Prod.instBornology` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.eq_empty_or_nonempty` `Set.prod_empty` `isBounded_prod_of_nonempty` `Set.Nonempty.prod`

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundedSpace_subtype` 📖	mathematical	`Bornology.IsBounded` `setOf`	`BoundedSpace` `instBornologySubtype`	—	`boundedSpace_subtype_iff`
`boundedSpace_val` 📖	mathematical	`Bornology.IsBounded`	`BoundedSpace` `Set.Elem` `instBornologySubtype` `Set` `Set.instMembership`	—	`boundedSpace_val_set_iff`
`fst_of_prod` 📖	—	`Bornology.IsBounded` `Prod.instBornology` `SProd.sprod` `Set` `Set.instSProd` `Set.Nonempty`	—	—	`image_fst` `Set.fst_image_prod`
`image_eval` 📖	mathematical	`Bornology.IsBounded` `Pi.instBornology`	`Set.image` `Function.eval`	—	`Bornology.forall_isBounded_image_eval_iff`
`image_fst` 📖	mathematical	`Bornology.IsBounded` `Prod.instBornology`	`Set.image`	—	`Bornology.isBounded_image_fst_and_snd`
`image_snd` 📖	mathematical	`Bornology.IsBounded` `Prod.instBornology`	`Set.image`	—	`Bornology.isBounded_image_fst_and_snd`
`pi` 📖	mathematical	`Bornology.IsBounded`	`Pi.instBornology` `Set.pi` `Set.univ`	—	`Bornology.forall_isBounded_image_eval_iff` `subset` `Set.eval_image_univ_pi_subset`
`prod` 📖	mathematical	`Bornology.IsBounded`	`Prod.instBornology` `SProd.sprod` `Set` `Set.instSProd`	—	`Bornology.isBounded_image_fst_and_snd` `subset` `Set.fst_image_prod_subset` `Set.snd_image_prod_subset`
`snd_of_prod` 📖	—	`Bornology.IsBounded` `Prod.instBornology` `SProd.sprod` `Set` `Set.instSProd` `Set.Nonempty`	—	—	`image_snd` `Set.snd_image_prod`

Pi

Definitions

Name	Category	Theorems
`instBornology` 📖	CompOp	12 math math: `BoxIntegral.Box.isBounded`, `instIsOrderBornology`, `Bornology.isBounded_pi_of_nonempty`, `Bornology.IsBounded.pi`, `bounded_stdSimplex`, `Bornology.forall_isBounded_image_eval_iff`, `BoxIntegral.Box.isBounded_Icc`, `Bornology.isBounded_pi`, `NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne`, `NumberField.mixedEmbedding.convexBodySum_isBounded`, `instBoundedSpaceForall`, `Bornology.cobounded_pi`

Prod

Definitions

Name	Category	Theorems
`instBornology` 📖	CompOp	11 math math: `Bornology.IsBounded.prod`, `Unitization.cobounded_eq_aux`, `instIsOrderBornology`, `instBoundedSpaceProd`, `Bornology.isBounded_image_fst_and_snd`, `Bornology.isBounded_prod`, `Bornology.isBounded_prod_self`, `NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne`, `NumberField.mixedEmbedding.convexBodySum_isBounded`, `Bornology.isBounded_prod_of_nonempty`, `Bornology.cobounded_prod`

(root)

Definitions

Name	Category	Theorems
`instBornologyAdditive` 📖	CompOp	1 math math: `instBoundedSpaceAdditive`
`instBornologyMultiplicative` 📖	CompOp	1 math math: `instBoundedSpaceMultiplicative`
`instBornologyOrderDual` 📖	CompOp	2 math math: `OrderDual.instIsOrderBornology`, `instBoundedSpaceOrderDual`
`instBornologySubtype` 📖	CompOp	6 math math: `Bornology.IsBounded.boundedSpace_subtype`, `Bornology.IsBounded.boundedSpace_val`, `boundedSpace_subtype_iff`, `Bornology.isBounded_image_subtype_val`, `boundedSpace_val_set_iff`, `instBoundedSpaceSubtype`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundedSpace_induced_iff` 📖	mathematical	—	`BoundedSpace` `Bornology.induced` `Bornology.IsBounded` `Set.range`	—	`Bornology.isBounded_univ` `Bornology.isBounded_induced` `Set.image_univ`
`boundedSpace_subtype_iff` 📖	mathematical	—	`BoundedSpace` `instBornologySubtype` `Bornology.IsBounded` `setOf`	—	`boundedSpace_induced_iff` `Subtype.range_coe_subtype`
`boundedSpace_val_set_iff` 📖	mathematical	—	`BoundedSpace` `Set.Elem` `instBornologySubtype` `Set` `Set.instMembership` `Bornology.IsBounded`	—	`boundedSpace_subtype_iff`
`instBoundedSpaceAdditive` 📖	mathematical	—	`BoundedSpace` `Additive` `instBornologyAdditive`	—	—
`instBoundedSpaceForall` 📖	mathematical	`BoundedSpace`	`Pi.instBornology`	—	`Bornology.cobounded_eq_bot` `Filter.coprodᵢ_bot`
`instBoundedSpaceMultiplicative` 📖	mathematical	—	`BoundedSpace` `Multiplicative` `instBornologyMultiplicative`	—	—
`instBoundedSpaceOrderDual` 📖	mathematical	—	`BoundedSpace` `OrderDual` `instBornologyOrderDual`	—	—
`instBoundedSpaceProd` 📖	mathematical	—	`BoundedSpace` `Prod.instBornology`	—	`Bornology.cobounded_eq_bot` `Filter.coprod_bot` `Filter.comap_bot`
`instBoundedSpaceSubtype` 📖	mathematical	—	`BoundedSpace` `instBornologySubtype`	—	`Bornology.IsBounded.boundedSpace_subtype` `Bornology.IsBounded.all`

---

← Back to Index