cardinality of insert

Stream: maths

[Jakob von Raumer]

Hi all, I'm fruitlessly trying to prove cardinal.mk ↥{x, y} ≤ ↑2, where {x, y} : set V. Is there a lemma on the cardinality of inserts that I'm just missing?

[Eric Wieser]

It's probably easier to show finset.card {x, y} ≤ 2, but it would be nice to know how to show your version too

[Jakob von Raumer]

Maybe the easiest way is to show that first and then lift the inequality to cardinal

[Jakob von Raumer]

(the latter part seems to be the more difficult half)

[Adam Topaz]

docs#set.card_insert

[Adam Topaz]

Oh, that has some fintype assumptions

[Adam Topaz]

There should be some lemma saying that if f : X \to Y is surjective, then the cardinality of Y is at most that of X. You can then use that and produce a surjection from fin 2 (maybe after a ulift?), for example

[Eric Rodriguez]

ahh, lean: image.png

[Eric Rodriguez]

(this is in cardinals, and the best solution that library_search suggests is norm_num.one_succ)

[Patrick Stevens]

What's the type of 2 and each of the 1 there?

[Patrick Stevens]

(I am still sore from the pain of equivocating between the real 2 and the nat 2 a lot recently)

[Patrick Stevens]

E.g. try have p : (2 : nat) = (1 : nat) + (1 : nat) := by norm_num and then convert p, you might get error messages telling you what's wrong

[Eric Rodriguez]

they're cardinals haha, but it ends up being okay ^^

[Eric Rodriguez]

import set_theory.cardinal
import data.fintype.card
import tactic.linarith

variables {α : Type*} [decidable_eq α]

instance set.fintype_insert'' {a : α} {s : set α} [fintype s] : fintype (insert a s : set α) :=
fintype.of_finset (insert a s.to_finset) $ by simp

example (x y : α) : cardinal.mk ({x, y} : set α) ≤ (2 : ℕ) :=
begin
  rw cardinal.fintype_card,
  norm_cast,
  obtain rfl | h := @eq_or_ne _ x y,
  { simp },
  rw set.card_insert,
  simp,
  simp [h]
end

this can definitely be improved

[Yakov Pechersky]

import set_theory.cardinal
import data.fintype.card
import tactic.linarith

variables {α : Type*}

lemma cardinal.mk_insert (s : set α) (x : α) :
  cardinal.mk (insert x s : set α) ≤ cardinal.mk s + 1 :=
begin
  rw ←set.union_singleton,
  convert cardinal.mk_union_le _ _,
  simp
end

example (x y : α) : cardinal.mk ({x, y} : set α) ≤ (2 : ℕ) :=
begin
  convert cardinal.mk_insert _ _,
  norm_num
end

[Eric Rodriguez]

(the simp is just rw cardinal.mk_singleton _, fwiw)

[Yaël Dillies]

And what about what we have in data.fintype.card_embedding? Sounds like it would be worth adding the contrapositive of fintype.card_embedding_eq_zero.

[Jakob von Raumer]

That's quite short in the end, thanks for the input, everyone!

[Jakob von Raumer]

I made it work with

{ rw [←@cardinal.finset_card V {x, y}],
                      apply cardinal.nat_cast_le.mpr,
                      transitivity, apply card_insert_le x {y},
                      rw [finset.card_singleton] }

[Jakob von Raumer]

If anyone is up to some :golf:, I couldnt find any better way to prove

f: fin 3 → V
⊢ range (fin.init f) = {f 0, f 1}

than to go down all the way to set extensionality and manually going through the cases on both sides...

[Johan Commelin]

I can't avoid ext either. This is my attempt so far:

open set

example {V : Type} (f : fin 3 → V) : range (fin.init f) = {f 0, f 1} :=
begin
  ext x, simp only [mem_singleton_iff, mem_range, mem_insert_iff, fin.init_def],
  split,
  { rintro ⟨x, rfl⟩, fin_cases x; simp, },
  { rintro (rfl|rfl); [use 0, use 1]; simp, }
end

[Jakob von Raumer]

Ah, rintro and especially fin_cases are tactics that I haven't found so far :)

[Jakob von Raumer]

ι : Type u_1
K : Type u_3
V : Type u
vs : ι → V
_inst_1: field K
_inst_2: add_comm_group V
_inst_3: module K V
hli : linear_independent K vs
⊢ linear_independent K ![vs i, vs i']

That's still missing in my proof that the projective space actually forms a projective geometry. Switching between entire families and fin-matrices is still quite awkward...

[Jakob von Raumer]

Nvm, I think I foud a nice way to circumvent this :)