Theorems · Theorem · convex and discrete geometry

AmpleSet.of_one_lt_codim

∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousSMul ℝ F] {E : Submodule ℝ F}, 1 < Module.rank ℝ (F ⧸ E) → AmpleSet (↑E)ᶜ

Let E be a linear subspace in a real vector space. If E has codimension at least two, its complement is ample.

Defined in

Mathlib.Analysis.Convex.AmpleSet

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul