michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

simplify proof of is_trunc_Grp

Browse source
This commit is contained in:
Floris van Doorn 2018-01-23 12:44:01 -05:00
parent d7b8530718
commit 6de6e72a03
2 changed files with 9 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
higher_groups.hlean
View file

@ -247,13 +247,8 @@ begin
apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y),
apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_equiv' X Y),
apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)),
apply is_trunc_pmap_of_is_conn X k.-2 (n + 1).-2 (n + k) Y,
{ clear X Y, induction k with k IH,
{ induction n with n IH,
{ apply le.refl },
{ exact trunc_index.succ_le_succ IH } },
{ rewrite (trunc_index.succ_add_plus_two (nat.succ k).-2 (n + 1).-2),
exact trunc_index.succ_le_succ IH } },
apply is_trunc_pmap_of_is_conn X k.-2 (n.-1) (n + k) Y,
{ apply le_of_eq, exact (sub_one_add_plus_two_sub_one n k)⁻¹ ⬝ !add_plus_two_comm },
{ exact _ }
end

7
move_to_lib.hlean
View file

@ -424,6 +424,13 @@ namespace trunc_index
{ exact !succ_add_plus_two ⬝ ap succ IH}
end
lemma sub_one_add_plus_two_sub_one (n m : ℕ) : n.-1 +2+ m.-1 = of_nat (n + m) :=
begin
induction m with m IH,
{ reflexivity },
{ exact ap succ IH }
end
end trunc_index
namespace int