We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 280bb33 commit 1f6d2faCopy full SHA for 1f6d2fa
classical/set_interval.v
@@ -860,7 +860,6 @@ Definition itv_closed_ends i : bool := itv_is_closed_unbounded i || itv_is_cc i.
860
861
End closed_endpoints.
862
863
-Arguments itv_open_ends {d T} !i /.
864
Lemma itv_open_endsI {d} {T : orderType d} (i j : interval T) :
865
itv_open_ends i -> itv_open_ends j -> itv_open_ends (i `&` j)%O.
866
Proof.
0 commit comments