CompactlyCoherentSpace

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

Statistics

Metric	Count
Definitions CompactlyCoherentSpace	1
Theorems isClosed_iff, isCoherentWith, isOpen_iff, isOpen_iff_forall_compactSpace, of_isClosed, of_isOpen, of_isOpen_forall_compactSpace, of_sequentialSpace, of_weaklyLocallyCompactSpace	9
Total	10

CompactlyCoherentSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_iff 📖	mathematical	—	IsClosed Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	Topology.IsCoherentWith.isClosed_iff isCoherentWith
isCoherentWith 📖	mathematical	—	Topology.IsCoherentWith setOf Set IsCompact	—	—
isOpen_iff 📖	mathematical	—	IsOpen Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	Topology.IsCoherentWith.isOpen_iff isCoherentWith
isOpen_iff_forall_compactSpace 📖	mathematical	—	IsOpen Set.preimage	—	IsOpen.preimage isOpen_iff isCompact_iff_compactSpace continuous_subtype_val
of_isClosed 📖	mathematical	IsClosed	CompactlyCoherentSpace	—	Topology.IsCoherentWith.of_isClosed
of_isOpen 📖	mathematical	IsOpen	CompactlyCoherentSpace	—	—
of_isOpen_forall_compactSpace 📖	mathematical	IsOpen	CompactlyCoherentSpace	—	of_isOpen Set.mem_range_self IsOpen.preimage Continuous.codRestrict isCompact_range Set.preimage_comp
of_sequentialSpace 📖	mathematical	—	CompactlyCoherentSpace	—	Topology.IsCoherentWith.of_seq Filter.Tendsto.isCompact_insert_range
of_weaklyLocallyCompactSpace 📖	mathematical	—	CompactlyCoherentSpace	—	Topology.IsCoherentWith.of_nhds WeaklyLocallyCompactSpace.exists_compact_mem_nhds

(root)

Definitions

Name	Category	Theorems
CompactlyCoherentSpace 📖	CompData	6 math math: to_compactlyCoherentSpace, CompactlyCoherentSpace.of_sequentialSpace, CompactlyCoherentSpace.of_isOpen_forall_compactSpace, CompactlyCoherentSpace.of_weaklyLocallyCompactSpace, CompactlyCoherentSpace.of_isClosed, CompactlyCoherentSpace.of_isOpen

---

← Back to Index