Theorem: Geometry.SimplicialComplex.face_dimension_le_space_dimension (LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ s.card ≤ FiniteDimensional.finrank 𝕜 E + 1
Tactic:
simpa using (K.indep hs).card_le_finrank_succ.trans (add_le_add_right (Submodule.finrank_le _) _)
State after:
no goals