CompactSystem

📁 Source: Mathlib/Topology/Compactness/CompactSystem.lean

Statistics

Metric	Count
Definitions IsCompactSystem	1
Theorems iff_nonempty_iInter, insert_empty, insert_univ, mono, nonempty_iInter, of_IsEmpty, of_nonempty_iInter, isCompactSystem_iff_nonempty_iInter_of_directed, isCompactSystem_iff_nonempty_iInter_of_lt, isCompactSystem_iff_of_directed, isCompactSystem_insert_empty_iff, isCompactSystem_insert_univ_iff, isCompactSystem_insert_univ_isCompact_isClosed, isCompactSystem_isCompact, isCompactSystem_isCompact_isClosed	15
Total	16

IsCompactSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_nonempty_iInter 📖	mathematical	—	IsCompactSystem Set.Nonempty Set.iInter	—	nonempty_iInter of_nonempty_iInter
insert_empty 📖	mathematical	IsCompactSystem	IsCompactSystem Set Set.instInsert Set.instEmptyCollection	—	Set.subset_empty_iff HasSubset.Subset.trans Set.instIsTransSubset Set.dissipate_subset le_rfl Eq.le Set.mem_of_mem_insert_of_ne Set.Nonempty.ne_empty
insert_univ 📖	mathematical	IsCompactSystem	IsCompactSystem Set Set.instInsert Set.univ	—	isEmpty_or_nonempty iff_nonempty_iInter Set.iInter_univ Mathlib.Tactic.Push.not_forall_eq Set.ext Set.subset_empty_iff LE.le.trans Set.antitone_dissipate
mono 📖	mathematical	IsCompactSystem Set Set.instHasSubset	IsCompactSystem	—	—
nonempty_iInter 📖	mathematical	IsCompactSystem Set Set.instMembership Set.Nonempty Set.dissipate	Set.Nonempty Set.iInter	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq
of_IsEmpty 📖	mathematical	—	IsCompactSystem	—	Set.eq_empty_of_isEmpty instIsEmptySubtype
of_nonempty_iInter 📖	mathematical	Set.Nonempty Set.iInter	IsCompactSystem	—	Mathlib.Tactic.Contrapose.contrapose₁

(root)

Definitions

Name	Category	Theorems
IsCompactSystem 📖	MathDef	14 math math: IsCompactSystem.iff_nonempty_iInter, isCompactSystem_isCompact, isCompactSystem_iff_nonempty_iInter_of_lt, isCompactSystem_iff_nonempty_iInter_of_directed, isCompactSystem_iff_of_directed, isCompactSystem_insert_univ_isCompact_isClosed, IsCompactSystem.of_IsEmpty, IsCompactSystem.insert_empty, IsCompactSystem.mono, isCompactSystem_insert_univ_iff, isCompactSystem_isCompact_isClosed, IsCompactSystem.insert_univ, isCompactSystem_insert_empty_iff, IsCompactSystem.of_nonempty_iInter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompactSystem_iff_nonempty_iInter_of_directed 📖	mathematical	IsPiSystem	IsCompactSystem Set.Nonempty Set.iInter	—	isCompactSystem_iff_of_directed Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq
isCompactSystem_iff_nonempty_iInter_of_lt 📖	mathematical	—	IsCompactSystem Set.Nonempty Set.iInter	—	Set.dissipate_eq_biInter_lt le_trans
isCompactSystem_iff_of_directed 📖	mathematical	IsPiSystem	IsCompactSystem Set Set.instEmptyCollection	—	isCompactSystem_insert_empty_iff Set.exists_dissipate_eq_empty_iff_of_directed IsPiSystem.dissipate_mem IsPiSystem.insert_empty Set.not_nonempty_iff_eq_empty Set.biInter_le_eq_iInter Set.directed_dissipate Mathlib.Tactic.Push.not_forall_eq
isCompactSystem_insert_empty_iff 📖	mathematical	—	IsCompactSystem Set Set.instInsert Set.instEmptyCollection	—	IsCompactSystem.mono Set.subset_insert IsCompactSystem.insert_empty
isCompactSystem_insert_univ_iff 📖	mathematical	—	IsCompactSystem Set Set.instInsert Set.univ	—	IsCompactSystem.mono Set.subset_insert IsCompactSystem.insert_univ
isCompactSystem_insert_univ_isCompact_isClosed 📖	mathematical	—	IsCompactSystem Set Set.instInsert Set.univ setOf IsCompact IsClosed	—	IsCompactSystem.insert_univ isCompactSystem_isCompact_isClosed
isCompactSystem_isCompact 📖	mathematical	—	IsCompactSystem setOf Set IsCompact	—	IsCompact.isClosed isCompactSystem_isCompact_isClosed
isCompactSystem_isCompact_isClosed 📖	mathematical	—	IsCompactSystem setOf Set IsCompact IsClosed	—	IsCompactSystem.of_nonempty_iInter Set.iInter_dissipate IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed Set.antitone_dissipate Set.dissipate_zero_nat isClosed_biInter

---

← Back to Index