Mathlib Map

Theorems · Theorem · global analysis

boundary_Icc

∀ {x y : ℝ} [hxy : Fact (x < y)], ModelWithCorners.boundary ↑(Set.Icc x y) = {⊥, ⊤}
Defined in
Mathlib.Geometry.Manifold.Instances.Real
Cited by
1 results in Mathlib
Foundations
Depth 231 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Fact
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

boundary_product · cited by 0boundary_productSet · cited by 53352SetReal · cited by 25697RealENNReal · cited by 9879ENNRealTop.top · cited by 9680Top.topSet.Elem · cited by 7166Set.ElemBot.bot · cited by 4720Bot.botFact · cited by 2726FactSet.ext · cited by 2266Set.extSet.Icc · cited by 1702Set.IccSet.Ioo · cited by 1214Set.IooEuclideanSpace · cited by 307EuclideanSpaceSet.mem_insert · cited by 109Set.mem_insertSet.mem_insert_of_mem · cited by 50Set.mem_insert_of_memEuclideanHalfSpace · cited by 47EuclideanHalfSpacemodelWithCornersEuclideanHalfSpace · cited by 35modelWithCornersEuclidean…boundary_IccCITED BYCITES

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Realstatement and proof · cited by 25,697
  • ENNRealstatement · cited by 9,879
  • Top.topstatement and proof · cited by 9,680
  • Set.Elemstatement and proof · cited by 7,166
  • Bot.botstatement and proof · cited by 4,720
  • Factstatement and proof · cited by 2,726
  • Set.extproof · cited by 2,266
  • Set.Iccstatement and proof · cited by 1,702
  • Set.Iooproof · cited by 1,214
  • EuclideanSpacestatement · cited by 307
  • Set.mem_insertproof · cited by 109

Cited by1

Results whose statement or proof uses this declaration.