Coherent

📁 Source: Mathlib/Topology/Coherent.lean

Statistics

Metric	Count
Definitions	0
Theorems continuous_iff, enlarge, isClosed_iff, isOpen_iff, mono, of_continuous_prop, of_isClosed, of_nhds, of_seq	9
Total	9

Topology.IsCoherentWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_iff 📖	mathematical	Topology.IsCoherentWith	Continuous ContinuousOn	—	Continuous.continuousOn continuous_def isOpen_iff IsOpen.preimage ContinuousOn.restrict
enlarge 📖	—	Topology.IsCoherentWith Set Set.instMembership Set.instHasSubset	—	—	of_continuous_prop continuous_iff ContinuousOn.mono
isClosed_iff 📖	mathematical	Topology.IsCoherentWith	IsClosed Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	isOpen_iff
isOpen_iff 📖	mathematical	Topology.IsCoherentWith	IsOpen Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	IsOpen.preimage continuous_subtype_val isOpen_of_forall_induced
mono 📖	—	Topology.IsCoherentWith Set Set.instHasSubset	—	—	enlarge Set.Subset.rfl
of_continuous_prop 📖	mathematical	Continuous sierpinskiSpace	Topology.IsCoherentWith	—	—
of_isClosed 📖	mathematical	IsClosed	Topology.IsCoherentWith	—	isClosed_compl_iff IsOpen.isClosed_compl
of_nhds 📖	mathematical	Set Set.instMembership Filter Filter.instMembership nhds	Topology.IsCoherentWith	—	of_continuous_prop continuous_iff_continuousAt ContinuousOn.continuousAt
of_seq 📖	mathematical	Set Set.instMembership Set.instInsert Set.range	Topology.IsCoherentWith	—	of_isClosed IsSeqClosed.isClosed isClosed_induced_iff IsClosed.mem_of_tendsto Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.Eventually.of_forall Set.ext_iff Subtype.preimage_val_eq_preimage_val_iff

---

← Back to Index