Documentation Verification Report

UpperLower

📁 Source: Mathlib/Analysis/Normed/Order/UpperLower.lean

Statistics

Metric	Count
Definitions	0
Theorems `lowerClosure_pi`, `upperClosure_pi`, `lowerClosure_pi`, `upperClosure_pi`, `cthickening`, `cthickening'`, `exists_subset_ball`, `mem_interior_of_forall_lt`, `thickening`, `thickening'`, `cthickening`, `cthickening'`, `exists_subset_ball`, `mem_interior_of_forall_lt`, `thickening`, `thickening'`, `closure_lowerClosure_comm_pi`, `closure_upperClosure_comm_pi`, `dist_anti_left_pi`, `dist_anti_right_pi`, `dist_inf_sup_pi`, `dist_le_dist_of_le_pi`, `dist_mono_left_pi`, `dist_mono_right_pi`, `lowerClosure_interior_subset`, `lowerClosure_interior_subset'`, `upperClosure_interior_subset`, `upperClosure_interior_subset'`	28
Total	28

IsClopen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lowerClosure_pi` 📖	mathematical	`IsClopen` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `BddAbove` `Pi.hasLe` `Real.instLE`	`SetLike.coe` `LowerSet` `Preorder.toLE` `Pi.preorder` `Real.instPreorder` `LowerSet.instSetLike` `lowerClosure`	—	`IsClosed.lowerClosure_pi` `IsOpen.lowerClosure` `IsOrderedAddMonoid.to_hasUpperLowerClosure` `Pi.isOrderedAddMonoid` `Real.instIsOrderedAddMonoid` `UniformContinuousConstVAdd.to_continuousConstVAdd` `IsUniformAddGroup.to_uniformContinuousConstVAdd` `Pi.instIsUniformAddGroup` `instIsUniformAddGroupReal`
`upperClosure_pi` 📖	mathematical	`IsClopen` `Pi.topologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `BddBelow` `Pi.hasLe` `Real.instLE`	`SetLike.coe` `UpperSet` `Preorder.toLE` `Pi.preorder` `Real.instPreorder` `UpperSet.instSetLike` `upperClosure`	—	`IsClosed.upperClosure_pi` `IsOpen.upperClosure` `IsOrderedAddMonoid.to_hasUpperLowerClosure` `Pi.isOrderedAddMonoid` `Real.instIsOrderedAddMonoid` `UniformContinuousConstVAdd.to_continuousConstVAdd` `IsUniformAddGroup.to_uniformContinuousConstVAdd` `Pi.instIsUniformAddGroup` `instIsUniformAddGroupReal`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lowerClosure_pi` 📖	mathematical	`BddAbove` `Pi.hasLe` `Real` `Real.instLE`	`IsClosed` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SetLike.coe` `LowerSet` `Preorder.toLE` `Pi.preorder` `Real.instPreorder` `LowerSet.instSetLike` `lowerClosure`	—	`nonempty_fintype` `IsSeqClosed.isClosed` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.instFirstCountableTopologyForallOfCountable` `Finite.to_countable` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Tendsto.bddBelow_range` `Pi.instBoundedGENhdsClass` `BoundedGENhdsClass.of_closedIicTopology` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `SemilatticeInf.instIsCodirectedOrder` `tendsto_subseq_of_bounded` `pi_properSpace` `instProperSpaceReal` `BddAbove.isBounded_inter` `Pi.instIsOrderBornology` `Real.instIsOrderBornology` `bddBelow_Ici` `LE.le.trans` `Set.mem_range_self` `closure_minimal` `Set.inter_subset_left` `le_of_tendsto_of_tendsto'` `Pi.orderClosedTopology'` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.comp` `StrictMono.tendsto_atTop`
`upperClosure_pi` 📖	mathematical	`BddBelow` `Pi.hasLe` `Real` `Real.instLE`	`IsClosed` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SetLike.coe` `UpperSet` `Preorder.toLE` `Pi.preorder` `Real.instPreorder` `UpperSet.instSetLike` `upperClosure`	—	`nonempty_fintype` `IsSeqClosed.isClosed` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.instFirstCountableTopologyForallOfCountable` `Finite.to_countable` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Tendsto.bddAbove_range` `Pi.instBoundedLENhdsClass` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `SemilatticeSup.instIsDirectedOrder` `tendsto_subseq_of_bounded` `pi_properSpace` `instProperSpaceReal` `BddBelow.isBounded_inter` `Pi.instIsOrderBornology` `Real.instIsOrderBornology` `bddAbove_Iic` `LE.le.trans` `Set.mem_range_self` `closure_minimal` `Set.inter_subset_left` `le_of_tendsto_of_tendsto'` `Pi.orderClosedTopology'` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.comp` `StrictMono.tendsto_atTop`

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cthickening` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`Metric.cthickening_eq_iInter_thickening''` `isLowerSet_iInter₂` `thickening`
`cthickening'` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedCommGroup.toMetricSpace`	—	`Metric.cthickening_eq_iInter_thickening''` `isLowerSet_iInter₂` `thickening'`
`exists_subset_ball` 📖	mathematical	`IsLowerSet` `Pi.hasLe` `Real` `Real.instLE` `Set` `Set.instMembership` `closure` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`Set.instHasSubset` `Metric.closedBall` `pseudoMetricSpacePi` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `interior`	—	`Nat.instAtLeastTwoHAddOfNat` `Metric.closedBall_subset_closedBall'` `dist_self_sub_left` `Function.const_def` `le_imp_le_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pi_norm_const_le` `le_refl` `le_of_eq` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_div` `Real.norm_ofNat` `abs_of_nonneg` `LT.lt.le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Metric.mem_closure_iff` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `zero_lt_four` `Real.instZeroLEOneClass` `NeZero.charZero_one` `mem_interior_of_forall_lt` `Finite.of_fintype` `subset_closure` `LE.le.trans` `norm_le_pi_norm` `dist_eq_norm` `dist_eq_norm'` `Metric.mem_closedBall` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `abs_sub_le_iff` `Mathlib.Meta.NormNum.isNat_lt_true` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `CancelDenoms.mul_subst`
`mem_interior_of_forall_lt` 📖	mathematical	`IsLowerSet` `Pi.hasLe` `Real` `Real.instLE` `Set` `Set.instMembership` `closure` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT`	`interior`	—	`nonempty_fintype` `Pi.exists_forall_pos_add_lt` `Real.instIsOrderedCancelAddMonoid` `Real.instNontrivial` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Metric.mem_closure_iff` `LT.lt.trans_le` `lt_sub_iff_add_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_le_comm` `LE.le.trans` `le_abs_self` `Real.norm_eq_abs` `dist_eq_norm` `LT.lt.le` `dist_pi_lt_iff` `mem_interior` `LT.lt.trans` `Real.ball_eq_Ioo` `ball_pi` `Set.mem_univ` `Metric.isOpen_ball` `Metric.mem_ball_self`
`thickening` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.thickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`ball_add_zero` `add_left`
`thickening'` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.thickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedCommGroup.toMetricSpace`	—	`ball_mul_one` `mul_left`

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cthickening` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`Metric.cthickening_eq_iInter_thickening''` `isUpperSet_iInter₂` `thickening`
`cthickening'` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedCommGroup.toMetricSpace`	—	`Metric.cthickening_eq_iInter_thickening''` `isUpperSet_iInter₂` `thickening'`
`exists_subset_ball` 📖	mathematical	`IsUpperSet` `Pi.hasLe` `Real` `Real.instLE` `Set` `Set.instMembership` `closure` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT` `Real.instZero`	`Set.instHasSubset` `Metric.closedBall` `pseudoMetricSpacePi` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `interior`	—	`Nat.instAtLeastTwoHAddOfNat` `Metric.closedBall_subset_closedBall'` `dist_self_add_left` `Function.const_def` `le_imp_le_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pi_norm_const_le` `le_refl` `le_of_eq` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_div` `Real.norm_ofNat` `abs_of_nonneg` `LT.lt.le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Metric.mem_closure_iff` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `zero_lt_four` `Real.instZeroLEOneClass` `NeZero.charZero_one` `mem_interior_of_forall_lt` `Finite.of_fintype` `subset_closure` `LE.le.trans` `norm_le_pi_norm` `dist_eq_norm` `dist_eq_norm'` `Metric.mem_closedBall` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `abs_sub_le_iff` `Mathlib.Meta.NormNum.isNat_lt_true` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `CancelDenoms.add_subst` `CancelDenoms.mul_subst`
`mem_interior_of_forall_lt` 📖	mathematical	`IsUpperSet` `Pi.hasLe` `Real` `Real.instLE` `Set` `Set.instMembership` `closure` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLT`	`interior`	—	`nonempty_fintype` `Pi.exists_forall_pos_add_lt` `Real.instIsOrderedCancelAddMonoid` `Real.instNontrivial` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Metric.mem_closure_iff` `LT.lt.trans_le'` `sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans` `le_abs_self` `Real.norm_eq_abs` `dist_eq_norm'` `LT.lt.le` `dist_pi_lt_iff` `mem_interior` `LT.lt.trans` `lt_sub_iff_add_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Real.ball_eq_Ioo` `ball_pi` `Set.mem_univ` `Metric.isOpen_ball` `Metric.mem_ball_self`
`thickening` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.thickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`ball_add_zero` `add_left`
`thickening'` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Metric.thickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedCommGroup.toMetricSpace`	—	`ball_mul_one` `mul_left`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_lowerClosure_comm_pi` 📖	mathematical	`BddAbove` `Pi.hasLe` `Real` `Real.instLE`	`closure` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SetLike.coe` `LowerSet` `Preorder.toLE` `Pi.preorder` `Real.instPreorder` `LowerSet.instSetLike` `lowerClosure`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_minimal` `lowerClosure_mono` `subset_closure` `IsClosed.lowerClosure_pi` `isClosed_closure` `BddAbove.closure` `instClosedIicTopology` `Pi.orderClosedTopology'` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `lowerClosure_min` `closure_mono` `subset_lowerClosure` `IsLowerSet.closure` `IsOrderedAddMonoid.to_hasUpperLowerClosure` `Pi.isOrderedAddMonoid` `Real.instIsOrderedAddMonoid` `UniformContinuousConstVAdd.to_continuousConstVAdd` `IsUniformAddGroup.to_uniformContinuousConstVAdd` `Pi.instIsUniformAddGroup` `instIsUniformAddGroupReal` `LowerSet.lower`
`closure_upperClosure_comm_pi` 📖	mathematical	`BddBelow` `Pi.hasLe` `Real` `Real.instLE`	`closure` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SetLike.coe` `UpperSet` `Preorder.toLE` `Pi.preorder` `Real.instPreorder` `UpperSet.instSetLike` `upperClosure`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `closure_minimal` `upperClosure_anti` `subset_closure` `IsClosed.upperClosure_pi` `isClosed_closure` `BddBelow.closure` `instClosedIciTopology` `Pi.orderClosedTopology'` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `upperClosure_min` `closure_mono` `subset_upperClosure` `IsUpperSet.closure` `IsOrderedAddMonoid.to_hasUpperLowerClosure` `Pi.isOrderedAddMonoid` `Real.instIsOrderedAddMonoid` `UniformContinuousConstVAdd.to_continuousConstVAdd` `IsUniformAddGroup.to_uniformContinuousConstVAdd` `Pi.instIsUniformAddGroup` `instIsUniformAddGroupReal` `UpperSet.upper`
`dist_anti_left_pi` 📖	mathematical	—	`AntitoneOn` `Real` `Pi.preorder` `Real.instPreorder` `Dist.dist` `PseudoMetricSpace.toDist` `pseudoMetricSpacePi` `Real.pseudoMetricSpace` `Set.Iic`	—	`NNReal.coe_le_coe` `Finset.sup_mono_fun` `Real.nndist_eq'` `Real.nnabs_of_nonneg` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.toNNReal_mono` `sub_le_sub_left`
`dist_anti_right_pi` 📖	mathematical	—	`AntitoneOn` `Real` `Pi.preorder` `Real.instPreorder` `Dist.dist` `PseudoMetricSpace.toDist` `pseudoMetricSpacePi` `Real.pseudoMetricSpace` `Set.Iic`	—	`dist_comm` `dist_anti_left_pi`
`dist_inf_sup_pi` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `pseudoMetricSpacePi` `Real` `Real.pseudoMetricSpace` `Pi.instMinForall_mathlib` `Real.instMin` `Pi.instMaxForall_mathlib` `Real.instMax`	—	`Finset.sup_congr` `Real.nndist_eq'` `max_sub_min_eq_abs` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Real.nnabs_of_nonneg` `Real.toNNReal_abs`
`dist_le_dist_of_le_pi` 📖	mathematical	`Pi.hasLe` `Real` `Real.instLE`	`Dist.dist` `PseudoMetricSpace.toDist` `pseudoMetricSpacePi` `Real.pseudoMetricSpace`	—	`LE.le.trans` `dist_mono_right_pi` `dist_anti_left_pi`
`dist_mono_left_pi` 📖	mathematical	—	`MonotoneOn` `Real` `Pi.preorder` `Real.instPreorder` `Dist.dist` `PseudoMetricSpace.toDist` `pseudoMetricSpacePi` `Real.pseudoMetricSpace` `Set.Ici`	—	`NNReal.coe_le_coe` `Finset.sup_mono_fun` `Real.nndist_eq` `Real.nnabs_of_nonneg` `sub_nonneg_of_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_imp_le_of_le_of_le` `Real.toNNReal_mono` `sub_le_sub_right` `le_refl`
`dist_mono_right_pi` 📖	mathematical	—	`MonotoneOn` `Real` `Pi.preorder` `Real.instPreorder` `Dist.dist` `PseudoMetricSpace.toDist` `pseudoMetricSpacePi` `Real.pseudoMetricSpace` `Set.Ici`	—	`dist_comm` `dist_mono_left_pi`
`lowerClosure_interior_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `LowerSet.instSetLike` `lowerClosure` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`lowerClosure_min` `interior_mono` `subset_lowerClosure` `IsLowerSet.interior` `IsOrderedAddMonoid.to_hasUpperLowerClosure` `IsIsometricVAdd.to_continuousConstVAdd` `NormedAddGroup.to_isIsometricVAdd_left` `LowerSet.lower`
`lowerClosure_interior_subset'` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `LowerSet.instSetLike` `lowerClosure` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `NormedCommGroup.toSeminormedCommGroup`	—	`lowerClosure_min` `interior_mono` `subset_lowerClosure` `IsLowerSet.interior` `IsOrderedMonoid.to_hasUpperLowerClosure` `IsIsometricSMul.to_continuousConstSMul` `NormedGroup.to_isIsometricSMul_left` `LowerSet.lower`
`upperClosure_interior_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `UpperSet.instSetLike` `upperClosure` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`upperClosure_min` `interior_mono` `subset_upperClosure` `IsUpperSet.interior` `IsOrderedAddMonoid.to_hasUpperLowerClosure` `IsIsometricVAdd.to_continuousConstVAdd` `NormedAddGroup.to_isIsometricVAdd_left` `UpperSet.upper`
`upperClosure_interior_subset'` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `UpperSet.instSetLike` `upperClosure` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedCommGroup.toPseudoMetricSpace` `NormedCommGroup.toSeminormedCommGroup`	—	`upperClosure_min` `interior_mono` `subset_upperClosure` `IsUpperSet.interior` `IsOrderedMonoid.to_hasUpperLowerClosure` `IsIsometricSMul.to_continuousConstSMul` `NormedGroup.to_isIsometricSMul_left` `UpperSet.upper`

---

← Back to Index