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	IsTransitiveRel Set.iInter	—	—
inter 📖	mathematical	IsTransitiveRel	IsTransitiveRel SetRel Set.instInter	—	—
mem_filter_prod_comm 📖	mathematical	SetRel Filter Filter.instMembership SProd.sprod Filter.instSProd	SetRel Filter Filter.instMembership SProd.sprod Filter.instSProd	—	mem_filter_prod_trans
mem_filter_prod_trans 📖	mathematical	SetRel Filter Filter.instMembership SProd.sprod Filter.instSProd	SetRel Filter Filter.instMembership SProd.sprod Filter.instSProd	—	Filter.Eventually.trans_prod SetRel.trans
preimage_prodMap 📖	mathematical	IsTransitiveRel	IsTransitiveRel Set.preimage	—	—
prod_subset_trans 📖	mathematical	Set Set.instHasSubset SProd.sprod Set.instSProd Set.Nonempty	Set Set.instHasSubset SProd.sprod Set.instSProd	—	SetRel.trans
sInter 📖	mathematical	IsTransitiveRel	IsTransitiveRel Set.sInter	—	Set.sInter_eq_iInter iInter
symmetrizeRel 📖	mathematical	IsTransitiveRel	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	9 math math: isTransitiveRel_singleton, IsTransitiveRel.inter, IsTransitiveRel.iInter, IsTransitiveRel.symmetrizeRel, IsTransitiveRel.preimage_prodMap, isTransitiveRel_iff_comp_subset_self, isTransitiveRel_univ, isTransitiveRel_empty, IsTransitiveRel.sInter
IsUltraUniformity 📖	CompData	15 math math: IsUltraUniformity.pi, IsUltraUniformity.bot, IsUltraUniformity.prod, IsUniformInducing.isUltraUniformity, IsUltraUniformity.completion, IsUltraUniformity.iInf, 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 📖	mathematical	Set Set.instMembership UniformSpace.ball	UniformSpace.ball	—	le_antisymm ball_subset_of_mem UniformSpace.mem_ball_symmetry
ball_subset_of_mem 📖	mathematical	Set Set.instMembership UniformSpace.ball	Set Set.instHasSubset UniformSpace.ball	—	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