Documentation Verification Report

Constructions

📁 Source: Mathlib/Topology/UniformSpace/Ultra/Constructions.lean

Statistics

Metric	Count
Definitions	0
Theorems `entourageProd`, `bot`, `comap`, `iInf`, `inf`, `pi`, `prod`, `top`, `isTrans_entourageProd`	9
Total	9

IsTransitiveRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`entourageProd` 📖	mathematical	—	`SetRel.IsTrans` `entourageProd`	—	`SetRel.isTrans_entourageProd`

IsUltraUniformity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot` 📖	mathematical	—	`IsUltraUniformity`	—	`Filter.hasBasis_principal` `mk_of_hasBasis` `DiscreteUniformity.eq_principal_setRelId` `SetRel.isSymm_id` `SetRel.isTrans_id`
`comap` 📖	mathematical	—	`IsUltraUniformity` `UniformSpace.comap`	—	`mk_of_hasBasis` `Filter.HasBasis.comap` `hasBasis` `SetRel.isSymm_preimage` `SetRel.isTrans_preimage`
`iInf` 📖	mathematical	`IsUltraUniformity`	`iInf` `UniformSpace` `instInfSetUniformSpace`	—	`mk_of_hasBasis` `Filter.HasBasis.iInf` `hasBasis` `iInf_uniformity` `Set.iInter_coe_set` `SetRel.isSymm_iInter` `SetRel.isTrans_iInter`
`inf` 📖	mathematical	—	`IsUltraUniformity` `UniformSpace` `instMinUniformSpace`	—	`mk_of_hasBasis` `Filter.HasBasis.inf` `hasBasis` `SetRel.isSymm_inter` `SetRel.isTrans_inter`
`pi` 📖	mathematical	`IsUltraUniformity`	`Pi.uniformSpace`	—	`iInf` `comap` `Pi.uniformSpace_eq`
`prod` 📖	mathematical	—	`IsUltraUniformity` `instUniformSpaceProd`	—	`inf` `comap`
`top` 📖	mathematical	—	`IsUltraUniformity` `Top.top` `UniformSpace` `instTopUniformSpace`	—	`Filter.hasBasis_top` `mk_of_hasBasis` `top_uniformity` `SetRel.isSymm_univ` `SetRel.isTrans_univ`

SetRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTrans_entourageProd` 📖	mathematical	—	`IsTrans` `entourageProd`	—	`trans`

---

← Back to Index