Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsTransitiveRel`, `IsUltraUniformity`	2
Theorems `comp_eq_of_idRel_subset`, `comp_subset_self`, `iInter`, `inter`, `mem_filter_prod_comm`, `mem_filter_prod_trans`, `preimage_prodMap`, `prod_subset_trans`, `sInter`, `symmetrizeRel`, `hasBasis`, `mem_nhds_iff_symm_trans`, `mk_of_hasBasis`, `isTopologicalBasis_clopens`, `isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity`, `isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity`, `isClosed_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity`, `isOpen_ball_of_mem_uniformity`, `nhds_basis_clopens`, `ball_eq_of_mem`, `ball_subset_of_mem`, `isTransitiveRel_empty`, `isTransitiveRel_iff_comp_subset_self`, `isTransitiveRel_singleton`, `isTransitiveRel_univ`	25
Total	27

IsTransitiveRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq_of_idRel_subset` 📖	mathematical	`IsTransitiveRel` `Set` `Set.instHasSubset` `idRel`	`SetRel.comp`	—	`le_antisymm` `comp_subset_self` `subset_comp_self`
`comp_subset_self` 📖	mathematical	`IsTransitiveRel`	`SetRel` `Set.instHasSubset` `SetRel.comp`	—	—
`iInter` 📖	mathematical	`IsTransitiveRel`	`Set.iInter`	—	—
`inter` 📖	mathematical	`IsTransitiveRel`	`SetRel` `Set.instInter`	—	—
`mem_filter_prod_comm` 📖	—	`SetRel` `Filter` `Filter.instMembership` `SProd.sprod` `Filter.instSProd`	—	—	`mem_filter_prod_trans`
`mem_filter_prod_trans` 📖	—	`SetRel` `Filter` `Filter.instMembership` `SProd.sprod` `Filter.instSProd`	—	—	`Filter.Eventually.trans_prod` `SetRel.trans`
`preimage_prodMap` 📖	mathematical	`IsTransitiveRel`	`Set.preimage`	—	—
`prod_subset_trans` 📖	—	`Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd` `Set.Nonempty`	—	—	`SetRel.trans`
`sInter` 📖	mathematical	`IsTransitiveRel`	`Set.sInter`	—	`Set.sInter_eq_iInter` `iInter`
`symmetrizeRel` 📖	mathematical	`IsTransitiveRel`	`SetRel.symmetrize`	—	—

IsUltraUniformity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBasis` 📖	mathematical	—	`Filter.HasBasis` `SetRel` `uniformity` `Filter` `Filter.instMembership` `SetRel.IsSymm` `SetRel.IsTrans`	—	—
`mem_nhds_iff_symm_trans` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `uniformity` `SetRel.IsSymm` `SetRel.IsTrans` `Set.instHasSubset` `UniformSpace.ball`	—	`UniformSpace.mem_nhds_iff` `Filter.HasBasis.mem_iff'` `hasBasis` `HasSubset.Subset.trans` `Set.instIsTransSubset` `UniformSpace.ball_mono`
`mk_of_hasBasis` 📖	mathematical	`Filter.HasBasis` `uniformity` `SetRel.IsSymm` `SetRel.IsTrans`	`IsUltraUniformity`	—	`Filter.HasBasis.to_hasBasis'` `Filter.HasBasis.mem_of_mem` `subset_rfl` `Set.instReflSubset`

TopologicalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTopologicalBasis_clopens` 📖	mathematical	—	`IsTopologicalBasis` `UniformSpace.toTopologicalSpace` `setOf` `Set` `IsClopen`	—	`IsTopologicalBasis.of_hasBasis_nhds` `UniformSpace.nhds_basis_clopens`

UniformSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity` 📖	mathematical	`SetRel` `Filter` `Filter.instMembership` `uniformity`	`IsClopen` `toTopologicalSpace` `ball`	—	`isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity` `isOpen_ball_of_mem_uniformity`
`isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity` 📖	mathematical	`SetRel` `Filter` `Filter.instMembership` `uniformity`	`IsClosed` `toTopologicalSpace` `ball`	—	`isOpen_compl_iff` `isOpen_iff_ball_subset` `SetRel.trans` `SetRel.symm`
`isClosed_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity` 📖	mathematical	`SetRel` `Filter` `Filter.instMembership` `uniformity`	`IsClosed` `toTopologicalSpace` `ball`	—	`isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity`
`isOpen_ball_of_mem_uniformity` 📖	mathematical	`SetRel` `Filter` `Filter.instMembership` `uniformity`	`IsOpen` `toTopologicalSpace` `ball`	—	`isOpen_iff_ball_subset` `ball_subset_of_mem`
`nhds_basis_clopens` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `toTopologicalSpace` `Set.instMembership` `IsClopen`	—	`Filter.HasBasis.to_hasBasis'` `nhds_basis_uniformity'` `IsUltraUniformity.hasBasis` `mem_ball_self` `isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity` `le_rfl` `IsOpen.mem_nhds_iff`

(root)

Definitions

Name	Category	Theorems
`IsTransitiveRel` 📖	MathDef	4 math math: `isTransitiveRel_singleton`, `isTransitiveRel_iff_comp_subset_self`, `isTransitiveRel_univ`, `isTransitiveRel_empty`
`IsUltraUniformity` 📖	CompData	13 math math: `IsUltraUniformity.bot`, `IsUltraUniformity.prod`, `IsUniformInducing.isUltraUniformity`, `IsUltraUniformity.completion`, `IsUltraUniformity.separationQuotient_iff`, `IsUltraUniformity.inf`, `IsUltraUniformity.separationQuotient`, `IsUltraUniformity.cauchyFilter`, `IsUltraUniformity.completion_iff`, `IsUltraUniformity.cauchyFilter_iff`, `IsUltraUniformity.mk_of_hasBasis`, `IsUltraUniformity.top`, `IsUltraUniformity.comap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_eq_of_mem` 📖	—	`Set` `Set.instMembership` `UniformSpace.ball`	—	—	`le_antisymm` `ball_subset_of_mem` `UniformSpace.mem_ball_symmetry`
`ball_subset_of_mem` 📖	mathematical	`Set` `Set.instMembership` `UniformSpace.ball`	`Set.instHasSubset`	—	`UniformSpace.ball_subset_of_comp_subset` `SetRel.comp_subset_self`
`isTransitiveRel_empty` 📖	mathematical	—	`IsTransitiveRel` `SetRel` `Set.instEmptyCollection`	—	—
`isTransitiveRel_iff_comp_subset_self` 📖	mathematical	—	`IsTransitiveRel` `SetRel` `Set.instHasSubset` `SetRel.comp`	—	`IsTransitiveRel.comp_subset_self`
`isTransitiveRel_singleton` 📖	mathematical	—	`IsTransitiveRel` `SetRel` `Set.instSingletonSet`	—	—
`isTransitiveRel_univ` 📖	mathematical	—	`IsTransitiveRel` `Set.univ`	—	—

---

← Back to Index