Cover

📁 Source: Mathlib/Data/Rel/Cover.lean

Statistics

Metric	Count
Definitions IsCover	1
Theorems anti, empty, mono, mono_entourage, nonempty, of_maximal_isSeparated, refl, rfl, union, isCover_empty_right, isCover_id, isCover_relId, isCover_univ	13
Total	14

SetRel

Definitions

Name	Category	Theorems
IsCover 📖	MathDef	10 math math: IsCover.of_maximal_isSeparated, isCover_univ, IsCover.refl, isCover_relId, UniformSpace.isCover_iff_subset_iUnion_ball, IsCover.rfl, IsCover.of_subset_iUnion_ball, isCover_id, isCover_empty_right, IsCover.empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCover_empty_right 📖	mathematical	—	IsCover Set Set.instEmptyCollection	—	—
isCover_id 📖	mathematical	—	IsCover id Set Set.instHasSubset	—	—
isCover_relId 📖	mathematical	—	IsCover id Set Set.instHasSubset	—	isCover_id
isCover_univ 📖	mathematical	—	IsCover Set.univ Set.Nonempty	—	—

SetRel.IsCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anti 📖	—	Set Set.instHasSubset SetRel.IsCover	—	—	—
empty 📖	mathematical	—	SetRel.IsCover Set Set.instEmptyCollection	—	instIsEmptyFalse
mono 📖	—	Set Set.instHasSubset SetRel.IsCover	—	—	—
mono_entourage 📖	—	SetRel Set.instHasSubset SetRel.IsCover	—	—	—
nonempty 📖	—	SetRel.IsCover Set.Nonempty	—	—	—
of_maximal_isSeparated 📖	mathematical	Maximal Set Set.instLE Set.instHasSubset SetRel.IsSeparated	SetRel.IsCover	—	SetRel.rfl Mathlib.Tactic.Push.not_and_eq SetRel.IsSeparated.insert Set.subset_insert Set.mem_insert
refl 📖	mathematical	—	SetRel.IsCover	—	SetRel.rfl
rfl 📖	mathematical	—	SetRel.IsCover	—	refl
union 📖	mathematical	SetRel.IsCover	Set Set.instUnion	—	—

---

← Back to Index