dim_le_of

Stream: Is there code for X?

[Kenny Lau]

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]

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]

this might be easier

[Kenny Lau]

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]

again I feel like it should have a shorter proof