Real

📁 Source: Mathlib/Geometry/Manifold/Instances/Real.lean

Statistics

Metric	Count
Definitions `EuclideanHalfSpace`, `EuclideanQuadrant`, `IccLeftChart`, `IccRightChart`, `term𝓡_`, `«term𝓡∂_»`, `instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc`, `instIccChartedSpace`, `instInhabitedEuclideanHalfSpace`, `instInhabitedEuclideanQuadrant`, `instTopologicalSpaceEuclideanHalfSpace`, `instTopologicalSpaceEuclideanQuadrant`, `instZeroEuclideanHalfSpace`, `instZeroEuclideanQuadrant`, `modelWithCornersEuclideanHalfSpace`, `modelWithCornersEuclideanQuadrant`	16
Theorems `convex`, `ext`, `ext_iff`, `pathConnectedSpace`, `convex`, `ext`, `ext_iff`, `pathConnectedSpace`, `instLeReal`, `IccLeftChart_extend_bot`, `IccLeftChart_extend_bot_mem_frontier`, `IccLeftChart_extend_interior_pos`, `IccRightChart_extend_top`, `IccRightChart_extend_top_mem_frontier`, `Icc_chartedSpaceChartAt`, `Icc_chartedSpaceChartAt_of_le_top`, `Icc_chartedSpaceChartAt_of_top_le`, `Icc_isBoundaryPoint_bot`, `Icc_isBoundaryPoint_top`, `Icc_isInteriorPoint_interior`, `boundary_Icc`, `boundary_product`, `closure_halfSpace`, `closure_open_halfSpace`, `frontier_halfSpace`, `frontier_range_modelWithCornersEuclideanHalfSpace`, `iccLeftChart_extend_zero`, `instIsManifoldIcc`, `instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc`, `instLocPathConnectedSpaceEuclideanHalfSpace`, `instLocPathConnectedSpaceEuclideanQuadrant`, `interior_euclideanQuadrant`, `interior_halfSpace`, `interior_range_modelWithCornersEuclideanHalfSpace`, `modelWithCornersEuclideanHalfSpace_zero`, `range_euclideanHalfSpace`, `range_euclideanQuadrant`, `range_modelWithCornersEuclideanHalfSpace`	38
Total	54

EuclideanHalfSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convex` 📖	mathematical	—	`Convex` `Real` `EuclideanSpace` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `WithLp.instSMul` `Function.hasSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `setOf` `Real.instLE` `Real.instZero` `WithLp.ofLp`	—	`fact_one_le_two_ennreal` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`ext` 📖	—	`EuclideanSpace` `Real` `Real.instLE` `Real.instZero` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	—	—
`ext_iff` 📖	mathematical	—	`EuclideanSpace` `Real` `Real.instLE` `Real.instZero` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ext`
`pathConnectedSpace` 📖	mathematical	—	`PathConnectedSpace` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace`	—	`isPathConnected_iff_pathConnectedSpace` `Convex.isPathConnected` `IsTopologicalAddGroup.toContinuousAdd` `fact_one_le_two_ennreal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `PiLp.instIsBoundedSMul` `Real.isBoundedSMul` `convex`

EuclideanQuadrant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convex` 📖	mathematical	—	`Convex` `Real` `EuclideanSpace` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `WithLp.instSMul` `Function.hasSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `setOf`	—	`fact_one_le_two_ennreal` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`ext` 📖	—	`EuclideanSpace` `Real`	—	—	—
`ext_iff` 📖	mathematical	—	`EuclideanSpace` `Real`	—	`ext`
`pathConnectedSpace` 📖	mathematical	—	`PathConnectedSpace` `EuclideanQuadrant` `instTopologicalSpaceEuclideanQuadrant`	—	`isPathConnected_iff_pathConnectedSpace` `Convex.isPathConnected` `IsTopologicalAddGroup.toContinuousAdd` `fact_one_le_two_ennreal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `PiLp.instIsBoundedSMul` `Real.isBoundedSMul` `convex`

Fact.Manifold

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLeReal` 📖	mathematical	—	`Fact` `Real` `Real.instLE`	—	`LT.lt.le` `Fact.out`

Manifold

Definitions

Name	Category	Theorems
`term𝓡_` 📖	CompOp	—
`«term𝓡∂_»` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`EuclideanHalfSpace` 📖	CompOp	33 math math: `instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc`, `Icc_isBoundaryPoint_bot`, `mfderivWithin_projIcc_one`, `Icc_isInteriorPoint_interior`, `mfderivWithin_comp_projIcc_one`, `IccLeftChart_extend_interior_pos`, `Icc_chartedSpaceChartAt_of_le_top`, `frontier_range_modelWithCornersEuclideanHalfSpace`, `EuclideanHalfSpace.pathConnectedSpace`, `contMDiff_subtype_coe_Icc`, `Icc_chartedSpaceChartAt`, `IccLeftChart_extend_bot`, `Manifold.riemannianEDist_def`, `modelWithCornersEuclideanHalfSpace_zero`, `contMDiffWithinAt_comp_projIcc_iff`, `Icc_chartedSpaceChartAt_of_top_le`, `oneTangentSpaceIcc_def`, `IccRightChart_extend_top_mem_frontier`, `instLocPathConnectedSpaceEuclideanHalfSpace`, `mdifferentiableWithinAt_comp_projIcc_iff`, `iccLeftChart_extend_zero`, `interior_range_modelWithCornersEuclideanHalfSpace`, `contMDiffOn_comp_projIcc_iff`, `Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc`, `range_modelWithCornersEuclideanHalfSpace`, `mfderiv_subtype_coe_Icc_one`, `IccRightChart_extend_top`, `boundary_Icc`, `boundary_product`, `IccLeftChart_extend_bot_mem_frontier`, `Icc_isBoundaryPoint_top`, `instIsManifoldIcc`, `contMDiffOn_projIcc`
`EuclideanQuadrant` 📖	CompOp	2 math math: `EuclideanQuadrant.pathConnectedSpace`, `instLocPathConnectedSpaceEuclideanQuadrant`
`IccLeftChart` 📖	CompOp	6 math math: `IccLeftChart_extend_interior_pos`, `Icc_chartedSpaceChartAt_of_le_top`, `Icc_chartedSpaceChartAt`, `IccLeftChart_extend_bot`, `iccLeftChart_extend_zero`, `IccLeftChart_extend_bot_mem_frontier`
`IccRightChart` 📖	CompOp	4 math math: `Icc_chartedSpaceChartAt`, `Icc_chartedSpaceChartAt_of_top_le`, `IccRightChart_extend_top_mem_frontier`, `IccRightChart_extend_top`
`instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc` 📖	CompOp	2 math math: `instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc`, `Manifold.riemannianEDist_def`
`instIccChartedSpace` 📖	CompOp	19 math math: `Icc_isBoundaryPoint_bot`, `mfderivWithin_projIcc_one`, `Icc_isInteriorPoint_interior`, `mfderivWithin_comp_projIcc_one`, `Icc_chartedSpaceChartAt_of_le_top`, `contMDiff_subtype_coe_Icc`, `Icc_chartedSpaceChartAt`, `contMDiffWithinAt_comp_projIcc_iff`, `Icc_chartedSpaceChartAt_of_top_le`, `oneTangentSpaceIcc_def`, `mdifferentiableWithinAt_comp_projIcc_iff`, `contMDiffOn_comp_projIcc_iff`, `Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc`, `mfderiv_subtype_coe_Icc_one`, `boundary_Icc`, `boundary_product`, `Icc_isBoundaryPoint_top`, `instIsManifoldIcc`, `contMDiffOn_projIcc`
`instInhabitedEuclideanHalfSpace` 📖	CompOp	—
`instInhabitedEuclideanQuadrant` 📖	CompOp	—
`instTopologicalSpaceEuclideanHalfSpace` 📖	CompOp	33 math math: `instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc`, `Icc_isBoundaryPoint_bot`, `mfderivWithin_projIcc_one`, `Icc_isInteriorPoint_interior`, `mfderivWithin_comp_projIcc_one`, `IccLeftChart_extend_interior_pos`, `Icc_chartedSpaceChartAt_of_le_top`, `frontier_range_modelWithCornersEuclideanHalfSpace`, `EuclideanHalfSpace.pathConnectedSpace`, `contMDiff_subtype_coe_Icc`, `Icc_chartedSpaceChartAt`, `IccLeftChart_extend_bot`, `Manifold.riemannianEDist_def`, `modelWithCornersEuclideanHalfSpace_zero`, `contMDiffWithinAt_comp_projIcc_iff`, `Icc_chartedSpaceChartAt_of_top_le`, `oneTangentSpaceIcc_def`, `IccRightChart_extend_top_mem_frontier`, `instLocPathConnectedSpaceEuclideanHalfSpace`, `mdifferentiableWithinAt_comp_projIcc_iff`, `iccLeftChart_extend_zero`, `interior_range_modelWithCornersEuclideanHalfSpace`, `contMDiffOn_comp_projIcc_iff`, `Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc`, `range_modelWithCornersEuclideanHalfSpace`, `mfderiv_subtype_coe_Icc_one`, `IccRightChart_extend_top`, `boundary_Icc`, `boundary_product`, `IccLeftChart_extend_bot_mem_frontier`, `Icc_isBoundaryPoint_top`, `instIsManifoldIcc`, `contMDiffOn_projIcc`
`instTopologicalSpaceEuclideanQuadrant` 📖	CompOp	2 math math: `EuclideanQuadrant.pathConnectedSpace`, `instLocPathConnectedSpaceEuclideanQuadrant`
`instZeroEuclideanHalfSpace` 📖	CompOp	1 math math: `modelWithCornersEuclideanHalfSpace_zero`
`instZeroEuclideanQuadrant` 📖	CompOp	—
`modelWithCornersEuclideanHalfSpace` 📖	CompOp	28 math math: `instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc`, `Icc_isBoundaryPoint_bot`, `mfderivWithin_projIcc_one`, `Icc_isInteriorPoint_interior`, `mfderivWithin_comp_projIcc_one`, `IccLeftChart_extend_interior_pos`, `frontier_range_modelWithCornersEuclideanHalfSpace`, `contMDiff_subtype_coe_Icc`, `IccLeftChart_extend_bot`, `Manifold.riemannianEDist_def`, `modelWithCornersEuclideanHalfSpace_zero`, `contMDiffWithinAt_comp_projIcc_iff`, `oneTangentSpaceIcc_def`, `IccRightChart_extend_top_mem_frontier`, `mdifferentiableWithinAt_comp_projIcc_iff`, `iccLeftChart_extend_zero`, `interior_range_modelWithCornersEuclideanHalfSpace`, `contMDiffOn_comp_projIcc_iff`, `Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc`, `range_modelWithCornersEuclideanHalfSpace`, `mfderiv_subtype_coe_Icc_one`, `IccRightChart_extend_top`, `boundary_Icc`, `boundary_product`, `IccLeftChart_extend_bot_mem_frontier`, `Icc_isBoundaryPoint_top`, `instIsManifoldIcc`, `contMDiffOn_projIcc`
`modelWithCornersEuclideanQuadrant` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IccLeftChart_extend_bot` 📖	mathematical	—	`PartialEquiv.toFun` `Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `EuclideanSpace` `OpenPartialHomeomorph.extend` `EuclideanHalfSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IccLeftChart` `modelWithCornersEuclideanHalfSpace` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Set.Icc.instOrderBotElemOfFactLe` `Fact.Manifold.instLeReal` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Real.instAddCommGroup`	—	`fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `sub_self`
`IccLeftChart_extend_bot_mem_frontier` 📖	mathematical	—	`EuclideanSpace` `Real` `Set` `Set.instMembership` `frontier` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.range` `EuclideanHalfSpace` `ModelWithCorners.toFun'` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `PartialEquiv.toFun` `Set.Elem` `Set.Icc` `Real.instPreorder` `OpenPartialHomeomorph.extend` `instTopologicalSpaceSubtype` `IccLeftChart` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Set.Icc.instOrderBotElemOfFactLe` `Fact.Manifold.instLeReal`	—	`fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `IccLeftChart_extend_bot` `frontier_range_modelWithCornersEuclideanHalfSpace` `Set.mem_setOf` `PiLp.zero_apply`
`IccLeftChart_extend_interior_pos` 📖	mathematical	`Real` `Real.instLT` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder`	`Real.instZero` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PartialEquiv.toFun` `Set.Elem` `EuclideanSpace` `OpenPartialHomeomorph.extend` `EuclideanHalfSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IccLeftChart` `modelWithCornersEuclideanHalfSpace`	—	`fact_one_le_two_ennreal` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`IccRightChart_extend_top` 📖	mathematical	—	`PartialEquiv.toFun` `Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `EuclideanSpace` `OpenPartialHomeomorph.extend` `EuclideanHalfSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IccRightChart` `modelWithCornersEuclideanHalfSpace` `Top.top` `OrderTop.toTop` `Preorder.toLE` `Set.Icc.instOrderTopElemOfFactLe` `Fact.Manifold.instLeReal` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Real.instAddCommGroup`	—	`fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `sub_self`
`IccRightChart_extend_top_mem_frontier` 📖	mathematical	—	`EuclideanSpace` `Real` `Set` `Set.instMembership` `frontier` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.range` `EuclideanHalfSpace` `ModelWithCorners.toFun'` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `PartialEquiv.toFun` `Set.Elem` `Set.Icc` `Real.instPreorder` `OpenPartialHomeomorph.extend` `instTopologicalSpaceSubtype` `IccRightChart` `Top.top` `OrderTop.toTop` `Preorder.toLE` `Set.Icc.instOrderTopElemOfFactLe` `Fact.Manifold.instLeReal`	—	`fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `IccRightChart_extend_top` `frontier_range_modelWithCornersEuclideanHalfSpace` `Set.mem_setOf` `PiLp.zero_apply`
`Icc_chartedSpaceChartAt` 📖	mathematical	—	`chartAt` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace` `OpenPartialHomeomorph` `Real.instLT` `Real.decidableLT` `IccLeftChart` `IccRightChart`	—	—
`Icc_chartedSpaceChartAt_of_le_top` 📖	mathematical	`Real` `Real.instLT` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder`	`chartAt` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `Set.Elem` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace` `IccLeftChart`	—	—
`Icc_chartedSpaceChartAt_of_top_le` 📖	mathematical	`Real` `Real.instLE` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder`	`chartAt` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `Set.Elem` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace` `IccRightChart`	—	`not_lt`
`Icc_isBoundaryPoint_bot` 📖	mathematical	—	`ModelWithCorners.IsBoundaryPoint` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `Set.Elem` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Set.Icc.instOrderBotElemOfFactLe` `Fact.Manifold.instLeReal`	—	`fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `ModelWithCorners.isBoundaryPoint_iff` `extChartAt.eq_1` `Icc_chartedSpaceChartAt_of_le_top` `Fact.out` `IccLeftChart_extend_bot_mem_frontier`
`Icc_isBoundaryPoint_top` 📖	mathematical	—	`ModelWithCorners.IsBoundaryPoint` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `Set.Elem` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace` `Top.top` `OrderTop.toTop` `Preorder.toLE` `Set.Icc.instOrderTopElemOfFactLe` `Fact.Manifold.instLeReal`	—	`fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `ModelWithCorners.isBoundaryPoint_iff` `extChartAt.eq_1` `Icc_chartedSpaceChartAt_of_top_le` `IccRightChart_extend_top_mem_frontier`
`Icc_isInteriorPoint_interior` 📖	mathematical	`Real` `Real.instLT` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder`	`ModelWithCorners.IsInteriorPoint` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `Set.Elem` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace`	—	`fact_one_le_two_ennreal` `ModelWithCorners.IsInteriorPoint.eq_1` `extChartAt.eq_1` `Icc_chartedSpaceChartAt_of_le_top` `interior_range_modelWithCornersEuclideanHalfSpace` `IccLeftChart_extend_interior_pos`
`boundary_Icc` 📖	mathematical	—	`ModelWithCorners.boundary` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `Set.Elem` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace` `Set.instInsert` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Set.Icc.instOrderBotElemOfFactLe` `Fact.Manifold.instLeReal` `Set.instSingletonSet` `Top.top` `OrderTop.toTop` `Set.Icc.instOrderTopElemOfFactLe`	—	`Set.ext` `fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `Set.eq_endpoints_or_mem_Ioo_of_mem_Icc` `SetCoe.ext` `Icc_isBoundaryPoint_bot` `Set.mem_insert` `Icc_isBoundaryPoint_top` `Set.mem_insert_of_mem` `ModelWithCorners.compl_boundary` `Icc_isInteriorPoint_interior`
`boundary_product` 📖	mathematical	—	`ModelWithCorners.boundary` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `Prod.normedAddCommGroup` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.normedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ModelProd` `EuclideanHalfSpace` `instTopologicalSpaceModelProd` `instTopologicalSpaceEuclideanHalfSpace` `ModelWithCorners.prod` `modelWithCornersEuclideanHalfSpace` `Set.Elem` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `prodChartedSpace` `instIccChartedSpace` `Set.prod` `Set.univ` `Set.instInsert` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Set.Icc.instOrderBotElemOfFactLe` `Fact.Manifold.instLeReal` `Set.instSingletonSet` `Top.top` `OrderTop.toTop` `Set.Icc.instOrderTopElemOfFactLe`	—	`fact_one_le_two_ennreal` `Fact.Manifold.instLeReal` `ModelWithCorners.boundary_of_boundaryless_left` `ModelWithCorners.instBoundarylessManifold` `boundary_Icc`
`closure_halfSpace` 📖	mathematical	—	`closure` `PiLp` `Real` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `setOf` `Real.instLE` `WithLp.ofLp`	—	`IsOpenMap.preimage_closure_eq_closure_preimage` `PiLp.isOpenMap_apply` `PiLp.continuous_apply` `closure_Ici` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`closure_open_halfSpace` 📖	mathematical	—	`closure` `PiLp` `Real` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `setOf` `Real.instLT` `WithLp.ofLp` `Real.instLE`	—	`IsOpenMap.preimage_closure_eq_closure_preimage` `PiLp.isOpenMap_apply` `PiLp.continuous_apply` `closure_Ioi` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`frontier_halfSpace` 📖	mathematical	—	`frontier` `PiLp` `Real` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `setOf` `Real.instLE` `WithLp.ofLp`	—	`frontier.eq_1` `closure_halfSpace` `interior_halfSpace` `Set.ext` `antisymm_iff` `instReflLe` `instAntisymmLe`
`frontier_range_modelWithCornersEuclideanHalfSpace` 📖	mathematical	—	`frontier` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.range` `EuclideanHalfSpace` `ModelWithCorners.toFun'` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `setOf` `Real.instZero` `WithLp.ofLp`	—	`fact_one_le_two_ennreal` `range_euclideanHalfSpace` `frontier_halfSpace` `Nat.instAtLeastTwoHAddOfNat`
`iccLeftChart_extend_zero` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PartialEquiv.toFun` `Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `EuclideanSpace` `OpenPartialHomeomorph.extend` `EuclideanHalfSpace` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `IccLeftChart` `modelWithCornersEuclideanHalfSpace` `Real.instSub`	—	`fact_one_le_two_ennreal`
`instIsManifoldIcc` 📖	mathematical	—	`IsManifold` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `Set.Elem` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instIccChartedSpace`	—	`fact_one_le_two_ennreal` `Nat.instAtLeastTwoHAddOfNat` `ContDiff.comp` `PiLp.contDiff_toLp` `ContDiff.add` `ContDiff.neg` `PiLp.contDiff_ofLp` `contDiff_const` `isManifold_of_contDiffOn` `mem_groupoid_of_pregroupoid` `symm_trans_mem_contDiffGroupoid` `ContDiffOn.congr` `ContDiff.contDiffOn` `PiLp.ext` `max_eq_left` `Function.update_self` `min_eq_left` `LT.lt.le` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `lt_sub_comm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc` 📖	mathematical	—	`IsManifold` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `Set.Elem` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc`	—	`fact_one_le_two_ennreal` `instIsManifoldIcc`
`instLocPathConnectedSpaceEuclideanHalfSpace` 📖	mathematical	—	`LocPathConnectedSpace` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace`	—	`Convex.locPathConnectedSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fact_one_le_two_ennreal` `IsBoundedSMul.continuousSMul` `PiLp.instIsBoundedSMul` `Real.isBoundedSMul` `NormedSpace.toLocallyConvexSpace` `EuclideanHalfSpace.convex`
`instLocPathConnectedSpaceEuclideanQuadrant` 📖	mathematical	—	`LocPathConnectedSpace` `EuclideanQuadrant` `instTopologicalSpaceEuclideanQuadrant`	—	`Convex.locPathConnectedSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `fact_one_le_two_ennreal` `IsBoundedSMul.continuousSMul` `PiLp.instIsBoundedSMul` `Real.isBoundedSMul` `NormedSpace.toLocallyConvexSpace` `EuclideanQuadrant.convex`
`interior_euclideanQuadrant` 📖	mathematical	—	`interior` `PiLp` `Real` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `setOf`	—	`Set.ext` `interior_iInter_of_finite` `Finite.of_fintype` `Set.iInter_congr` `IsOpenMap.preimage_interior_eq_interior_preimage` `PiLp.isOpenMap_apply` `PiLp.continuous_apply` `interior_Ici` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`interior_halfSpace` 📖	mathematical	—	`interior` `PiLp` `Real` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `setOf` `Real.instLE` `WithLp.ofLp` `Real.instLT`	—	`IsOpenMap.preimage_interior_eq_interior_preimage` `PiLp.isOpenMap_apply` `PiLp.continuous_apply` `interior_Ici` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`interior_range_modelWithCornersEuclideanHalfSpace` 📖	mathematical	—	`interior` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.range` `EuclideanHalfSpace` `ModelWithCorners.toFun'` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `setOf` `Real.instLT` `Real.instZero` `WithLp.ofLp`	—	`fact_one_le_two_ennreal` `range_euclideanHalfSpace` `interior_halfSpace`
`modelWithCornersEuclideanHalfSpace_zero` 📖	mathematical	—	`ModelWithCorners.toFun'` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EuclideanHalfSpace` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `instZeroEuclideanHalfSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Real.instAddCommGroup`	—	`fact_one_le_two_ennreal`
`range_euclideanHalfSpace` 📖	mathematical	—	`Set.range` `EuclideanSpace` `Real` `Real.instLE` `Real.instZero` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `setOf`	—	`Subtype.range_val`
`range_euclideanQuadrant` 📖	mathematical	—	`Set.range` `EuclideanSpace` `Real` `setOf`	—	`Subtype.range_val`
`range_modelWithCornersEuclideanHalfSpace` 📖	mathematical	—	`Set.range` `EuclideanSpace` `Real` `EuclideanHalfSpace` `ModelWithCorners.toFun'` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instTopologicalSpaceEuclideanHalfSpace` `modelWithCornersEuclideanHalfSpace` `setOf` `Real.instLE` `Real.instZero` `WithLp.ofLp`	—	`range_euclideanHalfSpace`

---

← Back to Index