## Stream: Is there code for X?

### Topic: dim_le_of

#### Kenny Lau (May 24 2020 at 15:14):

import linear_algebra.dimension

universes u v

variables {F : Type u} [field F] {K : Type v} [add_comm_group K] [vector_space F K]

theorem dim_le_of {n : ℕ} (H : ∀ s : finset K, linear_independent F (λ i : (↑s : set K), (i : K)) → s.card ≤ n) :
vector_space.dim F K ≤ n :=
_


#### Kenny Lau (May 24 2020 at 15:20):

this says that given a vector space K over a field F, if every linearly independent subset of K has size less than or equal to some given natural number n, then the F-dimension of K is less than or equal to n

#### Kenny Lau (May 24 2020 at 15:21):

this might be easier

#### Kenny Lau (May 24 2020 at 15:48):

import linear_algebra.dimension
import .cardinal

universes u v

variables {F : Type u} [field F] {K : Type v} [add_comm_group K] [vector_space F K]

theorem dim_le_of {n : ℕ} (H : ∀ s : finset K, linear_independent F (λ i : (↑s : set K), (i : K)) → s.card ≤ n) :
vector_space.dim F K ≤ n :=
let ⟨b, hb⟩ := exists_is_basis F K in
(vector_space.dim F K).lift_id ▸ hb.mk_eq_dim ▸ (cardinal.mk b).lift_id.symm ▸
card_le_of (λ s, @finset.card_map _ _ ⟨_, subtype.val_injective⟩ s ▸ H _
(by { refine linear_independent.mono (λ y h, _) hb.1,
rw [finset.mem_coe, finset.mem_map] at h, rcases h with ⟨x, hx, rfl⟩, exact x.2 } ))


#### Kenny Lau (May 24 2020 at 15:48):

again I feel like it should have a shorter proof

Last updated: May 07 2021 at 22:14 UTC