English
Let E be a real subspace of F with codimension at least two; its complement is ample.
Русский
Пусть E — подпространство в F с кодимензией по крайней мере два; его дополнение ампельно.
LaTeX
$$$\mathrm{of\_one\_lt\_codim} : 1 < \mathrm{rank}_{\mathbb{R}}(F/E) \Rightarrow \mathrm{AmpleSet}(E^c)$$$
Lean4
/-- Let `E` be a linear subspace in a real vector space.
If `E` has codimension at least two, its complement is ample. -/
theorem of_one_lt_codim [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {E : Submodule ℝ F}
(hcodim : 1 < Module.rank ℝ (F ⧸ E)) : AmpleSet (Eᶜ : Set F) := fun x hx ↦
by
rw [E.connectedComponentIn_eq_self_of_one_lt_codim hcodim hx, eq_univ_iff_forall]
intro y
by_cases h : y ∈ E
· obtain ⟨z, hz⟩ : ∃ z, z ∉ E := by
rw [← not_forall, ← Submodule.eq_top_iff']
rintro rfl
simp at hcodim
refine segment_subset_convexHull ?_ ?_ (mem_segment_sub_add y z) <;>
simpa [sub_eq_add_neg, Submodule.add_mem_iff_right _ h]
· exact subset_convexHull ℝ (Eᶜ : Set F) h
