Theorems · Theorem · global analysis

IccRightChart_extend_top_mem_frontier

∀ {x y : ℝ} [hxy : Fact (x < y)],
  ↑((IccRightChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊤ ∈
    frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace 1))

Defined in: Mathlib.Geometry.Manifold.Instances.Real
Cited by: 1 results in Mathlib
Foundations: Depth 229 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites20

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
Realstatement and proof · cited by 25,697
ENNRealstatement · cited by 9,879
Top.topstatement · cited by 9,680
Set.Elemstatement · cited by 7,166
Set.rangestatement and proof · cited by 4,705
Factstatement and proof · cited by 2,726
Set.Iccstatement · cited by 1,702
PartialEquiv.toFunstatement · cited by 821
ModelWithCorners.toFun'statement and proof · cited by 373
EuclideanSpacestatement and proof · cited by 307
frontierstatement and proof · cited by 214

Cited by1

Results whose statement or proof uses this declaration.

Icc_isBoundaryPoint_topproof · cited by 1