Skip to content
Snippets Groups Projects
Commit dc3b0de3 authored by François Clément's avatar François Clément
Browse files

Equiv -> impl.

parent 71731d6c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
Lebesgue/Subset_Rbar.v
+ 1
− 1
View file @ dc3b0de3
......@@ -913,7 +913,7 @@ Proof.
apply Ext_equiv; split; intros B HB.
(* *)
induction HB as [A HA | B HB].
apply R_Rbar_open_equiv; easy.
apply open_R_Rbar; easy.
induction HB as [A B1 HA HB1 | A a b HA]; repeat apply open_or.
1,3: apply R_Rbar_open_equiv; easy.
1,2,3: apply Rbar_ray_open_is_open; try easy.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment