Theorems · Theorem · functional analysis
IsOpen.exists_between_affineIndependent_span_eq_top
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P] {s u : Set P},
IsOpen u →
s ⊆ u →
s.Nonempty →
AffineIndependent ℝ Subtype.val → ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤Given a set s of affine-independent points belonging to an open set u, we may extend s to
an affine basis, all of whose elements belong to u.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites49
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Top.topstatement and proof · cited by 9,680
- Set.Elemproof · cited by 7,166
- Norm.normproof · cited by 5,413
- Set.rangeproof · cited by 4,705
- Unitsproof · cited by 2,804
- Set.Nonemptystatement and proof · cited by 2,627
- IsOpenstatement and proof · cited by 2,400
Cited by1
Results whose statement or proof uses this declaration.
- IsOpen.exists_subset_affineIndependent_span_eq_topproof · cited by 1