Zulip Chat Archive

Stream: Is there code for X?

Topic: dim_le_of


view this post on Zulip 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 :=
_

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 24 2020 at 15:21):

this might be easier

view this post on Zulip 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 } ))

view this post on Zulip 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