Theorems · Definition · convex and discrete geometry

intrinsicFrontier

(𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring 𝕜] →
        [inst_1 : AddCommGroup V] → [Module 𝕜 V] → [TopologicalSpace P] → [AddTorsor V P] → Set P → Set P

The intrinsic frontier of a set is its frontier considered as a set in its affine span.

Defined in

Mathlib.Analysis.Convex.Intrinsic

Cited by

21 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleTopologicalSpaceAddTorsor