Documentation Verification Report

Visible

📁 Source: Mathlib/Analysis/Convex/Visible.lean

Statistics

Metric	Count
Definitions `IsVisible`	1
Theorems `convexHull_subset_affineSpan_isVisible`, `exists_wbtw_isVisible`, `eq_of_isVisible_of_left_mem`, `eq_of_mem_interior`, `mem_convexHull_isVisible`, `mono`, `of_convexHull_of_pos`, `rfl`, `isVisible_comm`, `isVisible_iff_lineMap`, `rank_le_card_isVisible`	11
Total	12

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexHull_subset_affineSpan_isVisible` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid`	`Set.instHasSubset` `SetLike.coe` `AffineSubspace` `Real.instRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineSubspace.instSetLike` `affineSpan` `Set.instUnion` `Set.instSingletonSet` `setOf` `IsVisible` `Real.instField` `Real.linearOrder`	—	`exists_wbtw_isVisible` `AffineSubspace.right_mem_of_wbtw` `subset_affineSpan` `Set.subset_union_left` `affineSpan_mono` `Set.subset_union_right` `convexHull_subset_affineSpan` `IsVisible.mem_convexHull_isVisible`
`exists_wbtw_isVisible` 📖	mathematical	`Set` `Set.instMembership`	`Wbtw` `Real` `Real.instRing` `Real.partialOrder` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `IsVisible` `Real.instField` `Real.linearOrder`	—	`Real.instZeroLEOneClass` `AffineMap.lineMap_apply_one` `BddBelow.inter_of_left` `bddBelow_Ici` `csInf_le` `csInf_mem` `instOrderTopologyReal` `inter` `isClosed_Ici` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `preimage` `AffineMap.lineMap_continuous` `instIsTopologicalAddTorsor` `wbtw_lineMap_iff` `Real.instIsOrderedRing` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LE.le.lt_of_ne'` `AffineMap.lineMap_apply_zero` `AffineMap.lineMap_same` `LE.le.lt_of_ne` `LE.le.not_gt` `mul_nonneg` `IsOrderedRing.toPosMulMono` `LT.lt.le` `AffineMap.lineMap_lineMap_right` `mul_lt_of_lt_one_left` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_isVisible_of_left_mem` 📖	—	`IsOpen` `IsVisible` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Set` `Set.instMembership`	—	—	`IsVisible.eq_of_mem_interior` `interior_eq`

IsVisible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_mem_interior` 📖	—	`IsVisible` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Set` `Set.instMembership` `interior`	—	—	`Filter.Tendsto.eventually_mem` `Continuous.continuousWithinAt` `AffineMap.lineMap_continuous` `instIsTopologicalAddTorsor` `AffineMap.lineMap_apply_zero` `mem_interior_iff_mem_nhds` `Filter.mp_mem` `Ioo_mem_nhdsGT` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Filter.univ_mem'` `symm` `IsStrictOrderedRing.toIsOrderedRing` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Filter.Eventually.exists` `nhdsGT_neBot` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instNoMaxOrderOfNontrivial` `EuclideanDomain.toNontrivial`
`mem_convexHull_isVisible` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `IsVisible` `Real.instField` `Real.linearOrder` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup`	`setOf`	—	`mem_convexHull_iff_exists_fintype` `Real.instIsStrictOrderedRing` `Fintype.sum_subset` `Finset.mem_filter` `Finset.mem_univ` `left_ne_zero_of_smul` `Convex.sum_mem` `convex_convexHull` `Finset.sum_filter_ne_zero` `subset_convexHull` `of_convexHull_of_pos` `LE.le.lt_of_ne'`
`mono` 📖	—	`Set` `Set.instHasSubset` `IsVisible`	—	—	—
`of_convexHull_of_pos` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `IsVisible` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset` `Finset.instMembership` `Preorder.toLT`	—	—	`eq_or_lt_of_le` `LE.le.trans_eq` `Finset.single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `one_smul` `Finset.sum_eq_single` `Finset.sum_eq_zero_iff_of_nonneg` `Finset.erase_subset` `Finset.sum_erase_eq_sub` `sub_eq_zero` `Finset.mem_erase` `zero_smul` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `instIsEmptyFalse` `LE.le.lt_of_ne` `AffineMap.lineMap_apply_zero` `AffineMap.lineMap_apply_one` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `add_pos'` `Mathlib.Meta.Positivity.pos_of_isNat` `EuclideanDomain.toNontrivial` `div_le_one` `zero_add` `add_zero` `add_le_add` `covariant_swap_add_of_covariant_add` `add_le_add_left` `Finset.smul_sum` `Finset.sum_congr` `smul_smul` `mul_div_cancel₀` `LT.lt.ne'` `Finset.add_sum_erase` `AffineMap.lineMap_apply_module` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `mul_pos` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.mul_congr` `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_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `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.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Convex.mem_of_wbtw` `convex_convexHull` `Convex.sum_mem` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `Finset.sum_div` `div_self` `subset_convexHull` `sbtw_lineMap_iff` `inv_pos_of_pos` `div_lt_one` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd`
`rfl` 📖	mathematical	—	`IsVisible`	—	—

(root)

Definitions

Name	Category	Theorems
`IsVisible` 📖	MathDef	6 math math: `rank_le_card_isVisible`, `IsClosed.exists_wbtw_isVisible`, `isVisible_iff_lineMap`, `IsClosed.convexHull_subset_affineSpan_isVisible`, `IsVisible.rfl`, `isVisible_comm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isVisible_comm` 📖	mathematical	—	`IsVisible`	—	—
`isVisible_iff_lineMap` 📖	mathematical	—	`IsVisible` `Set` `Set.instMembership` `DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	—	`instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`rank_le_card_isVisible` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid`	`Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `addGroupIsAddTorsor` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Submodule.addCommMonoid` `Submodule.module` `Set.Elem` `setOf` `IsVisible` `Real.instField` `Real.linearOrder`	—	`Submodule.rank_mono` `Submodule.span_mono` `Set.vadd_set_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_convexHull` `IsClosed.convexHull_subset_affineSpan_isVisible` `AffineSubspace.pointwise_vadd_span` `Set.vadd_set_insert` `neg_add_cancel` `affineSpan_insert_zero` `AffineSubspace.coe_pointwise_vadd` `Submodule.span_span` `rank_span_le` `IsNoetherianRing.strongRankCondition` `Real.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Cardinal.mk_vadd_set`

---

← Back to Index