Theorems · Definition · general topology
frontier
{X : Type u} → [TopologicalSpace X] → Set X → Set XThe frontier of a set is the set of points between the closure and interior.
- Defined in
- Mathlib.Topology.Defs.Basic
- Cited by
- 214 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 34 definitions · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- closureproof · cited by 1,254
- interiorproof · cited by 714
Cited by220
Results whose statement or proof uses this declaration.
- intrinsicFrontierproof · cited by 21
- frontier_eq_closure_inter_closurestatement and proof · cited by 12
- ModelWithCorners.IsBoundaryPointproof · cited by 11
- frontier_complstatement · cited by 10
- frontier_le_subset_eqstatement · cited by 6
- frontier_subset_closurestatement · cited by 6
- IsOpenMap.preimage_frontier_eq_frontier_preimagestatement · cited by 6
- isClopen_iff_frontier_eq_emptystatement and proof · cited by 6
- ModelWithCorners.isBoundaryPoint_iffstatement · cited by 5
- closure_sdiff_interiorstatement · cited by 5
- OpenPartialHomeomorph.piecewisestatement and proof · cited by 4
- HasSmallInductiveDimensionLT.monoproof · cited by 4
Showing the 200 most cited of 220.