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

chore(data/set): cleanup proofs to make them less dependent on unifier heuristics

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-09 18:46:23 -08:00
parent 5e14b4ebe8
commit 0c4a6d3c5e
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/data/set/filter.lean
View file

@ -401,6 +401,7 @@ le.antisymm !bot_le
begin begin
apply le_of_forall_eventually, apply le_of_forall_eventually,
intro P H, intro P H,
unfold eventually,
apply mem_univ apply mem_univ
end end

6
library/data/set/map.lean
View file

@ -121,8 +121,10 @@ inj_on_of_left_inv_on H
theorem left_inverse_comp {f' : map b a} {g' : map c b} {g : map b c} {f : map a b} theorem left_inverse_comp {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
(Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) : (Hf : map.left_inverse f' f) (Hg : map.left_inverse g' g) :
map.left_inverse (f' ∘ g') (g ∘ f) := map.left_inverse (f' ∘ g') (g ∘ f) :=
left_inv_on_comp (mapsto f) Hf Hg begin
unfold map.left_inverse,
exact left_inv_on_comp (mapsto f) Hf Hg
end
/- right inverse -/ /- right inverse -/
-- g is a right inverse to f -- g is a right inverse to f