## Stream: new members

### Topic: injective function

#### Busiso Chisala (Nov 05 2020 at 12:21):

Is there an easy way to formulate/prove the existence of an injective function from finite set A to B given that the cardinalities (?) allow? The choose-using tactic will give a function (I guess) but ... I have the idea that a finset induction would do it, but worry there is a trivial way out there will save me the trouble. I want to use this in the 'extend to a basis' manner. Thanks

#### Kevin Buzzard (Nov 05 2020 at 12:22):

Can you formalise the precise statement which you want?

#### Kevin Buzzard (Nov 05 2020 at 12:23):

"finite set" can be said in several different ways in Lean and the answer to your question is probably "yes", but the details will depend on precisely how you want to state the maths assertion in type theory.

#### Kevin Buzzard (Nov 05 2020 at 12:24):

One thing I learnt very early on is that formalising the question is an important part of asking the question.

#### Kevin Buzzard (Nov 05 2020 at 12:26):

Another thing I learnt very early on is that choosing a random way to formalise the question and then solving it might lead to problems later when I want to apply the theorem I've already proved. I might find that it doesn't apply, because set.finite and fintype and finset are all different things.

#### Kevin Buzzard (Nov 05 2020 at 12:28):

In set theory, a set is a primitive notion and there is no question about what is meant. In type theory the type is the primitive notion, and various concepts of finite set can be built on top of this in different ways.

#### Busiso Chisala (Nov 05 2020 at 13:25):

An fintype indexed set of vectors v: ι → E some of which are zero, the rest linearly independent. Say on sets s,t :finset ι, respectively. Suppose that the dimension of E is |s|+|t| and I have a ready set of |s| vectors to complete my basis (say via a w: k → E). I suppose I am not very happy with how fin m objects work ... My use case is v: fin n → E. Must I really ?

#### Kevin Buzzard (Nov 05 2020 at 13:27):

Can you make a #mwe? A self-contained piece of code containing one sorry which is what you want filled in? This is the precise meaning of my original question.

#### Kevin Buzzard (Nov 05 2020 at 13:28):

This is an important skill to learn.

I'll try

#### Busiso Chisala (Nov 05 2020 at 15:26):

I had some trouble, so this exercise was well worth it:

variables {n E:Type} [fintype n] [inner_product_space ℝ E] [finite_dimensional ℝ E]

-- rather than use 'fin k → E' I have used fintype n for illustration

local notation ⟪x, y⟫ := @inner ℝ _ _ x y

-- to simplify my statements

def is_orth (v: n → E) : Prop := ∀ i j:n, i ≠ j → ⟪v i, v j⟫=0

def is_nonzero (v: n → E) : Prop := ∀ i:n,  v i ≠ 0

def enlarges (v: n → E) (w: n → E) : Prop := ∀ i:n, v i ≠ 0 → w i = v i

example {v: n → E} (ho: is_orth v) : ∃ w: n → E, enlarges v w  ∧ is_orth w  ∧  is_nonzero w :=
begin
let s := { i ∈ (finset.univ : finset n) | v i = 0 },
have : ∃ z:fin (s.card) → E, is_orth z ∧ is_nonzero z := sorry ,
-- would like to use z, which we can engineer to be in the orthogonal to v.range
cases this with z hz,
-- how to interweave z with v ?
sorry
end


? use .val?

#### Kevin Buzzard (Nov 06 2020 at 11:42):

Here's what I came up with:

import data.fintype.basic

variables { m p :Type } [fintype m] [fintype p]

open fintype

example  {s: finset m} {h: s.card = fintype.card p} :
∃ f: p → m, function.injective f ∧ ∀ i:m, i ∈ s → ∃ t:p, i=f t :=
begin
let S := {x : m // x ∈ s},
have hS : fintype.card S = s.card,
apply subtype_card, simp,
rw [h, fintype.card_eq] at hS,
cases hS with e,
-- e is a bijection S -> p
use (λ x, e.symm x),
split,
{ intros x y hxy,
apply equiv.injective e.symm,
exact subtype.ext hxy },
{ intros i hi,
use e ⟨i, hi⟩,
simp }
end


#### Kevin Buzzard (Nov 06 2020 at 11:43):

Looking around in the library I found fintype.card_eq which says that if two fintypes have the same cardinality then there's an equiv between them, i.e. a bijection. I built the proof on that.

#### Kevin Buzzard (Nov 06 2020 at 11:44):

s is a finset so it's not a type, it's a term. The corresponding type is S.

#### Busiso Chisala (Nov 06 2020 at 13:38):

Kevin Buzzard said:

Looking around in the library I found fintype.card_eq which says that if two fintypes have the same cardinality then there's an equiv between them, i.e. a bijection. I built the proof on that.

Thanks ! I was about to moot an induction. This clears quite a few things :+1:

#### Eric Wieser (Nov 06 2020 at 14:23):

Can you use coe_sort s as the type instead rather than defining S? I can never remember how to input the coe_sort up arrow...

#### Kevin Buzzard (Nov 06 2020 at 17:51):

Probably -- but I have exactly the same problem!

#### Eric Wieser (Nov 07 2020 at 11:42):

Usually I resort to finding a lemma that does a coercion, and copying it from the goal window...

Last updated: Dec 20 2023 at 11:08 UTC