Skip to content

Commit

Permalink
clean normedtype
Browse files Browse the repository at this point in the history
  • Loading branch information
@mkerjean
mkerjean committed Aug 22, 2024
1 parent 8bef47d commit a1fe712
Showing 1 changed file with 0 additions and 8 deletions.
8 changes: 0 additions & 8 deletions theories/normedtype.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2406,14 +2406,6 @@ Qed.
(** Continuity of norm *)
End NVS_continuity_normedModType.

Lemma regular_Uniform_isEvt (R : numFieldType) : Uniform_isEvt R R^o.
Proof.
split.

Search "cont" (GRing.add).



Section NVS_continuity_mul.

Context {K : numFieldType}.
Expand Down

0 comments on commit a1fe712

Please sign in to comment.