Complex vector spaces #1692
Complex vector spaces #1692
Conversation
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
Outdated
Show resolved
Hide resolved
src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
Outdated
Show resolved
Hide resolved
fredrik-bakke
left a comment
fredrik-bakke
left a comment
There was a problem hiding this comment.
I think you should write new files on positive intervals, negative intervals, and their interaction so that you can in particular avoid these long and awkward type signatures.
| same-sign-a-c = | ||
| same-sign-is-positive-mul-ℚ | ||
| ( is-positive-leq-ℚ⁺ | ||
| ( _ , is-pos-lb) | ||
| ( transitive-leq-ℚ _ _ _ (leq-left-min-ℚ _ _) (leq-left-min-ℚ _ _))) | ||
| same-sign-a-d = | ||
| same-sign-is-positive-mul-ℚ | ||
| ( is-positive-leq-ℚ⁺ | ||
| ( _ , is-pos-lb) | ||
| ( transitive-leq-ℚ _ _ _ | ||
| ( leq-right-min-ℚ _ _) | ||
| ( leq-left-min-ℚ _ _))) | ||
| same-sign-b-d = | ||
| same-sign-is-positive-mul-ℚ | ||
| ( is-positive-leq-ℚ⁺ | ||
| ( _ , is-pos-lb) | ||
| ( transitive-leq-ℚ _ _ _ | ||
| ( leq-right-min-ℚ _ _) | ||
| ( leq-right-min-ℚ _ _))) |
There was a problem hiding this comment.
These should be separate lemmas: same-sign-lower-bound-is-positive-mul-closed-interval-ℚ, same-sign-upper-lower-bound-is-positive-mul-closed-interval-ℚ, and same-sign-upper-bound-is-positive-mul-closed-interval-ℚ respectively
| is-neg-d = | ||
| rec-coproduct | ||
| ( pr2) | ||
| ( λ (is-pos-a , _) → | ||
| ex-falso | ||
| ( is-not-negative-and-positive-ℚ (is-neg-a , is-pos-a))) | ||
| ( same-sign-a-d) | ||
| is-neg-b = | ||
| rec-coproduct | ||
| ( pr1) | ||
| ( λ (_ , is-pos-d) → | ||
| ex-falso | ||
| ( is-not-negative-and-positive-ℚ (is-neg-d , is-pos-d))) | ||
| ( same-sign-b-d) |
There was a problem hiding this comment.
can these be factored into separate lemmas of the form not-same-sign-BLAH-BLAH-is-positive-mul-closed-interval-ℚ
There was a problem hiding this comment.
Sorry, I mean *is-negative-upper-bound-right-factor-is-positive-mul-closed-interval-ℚ and is-negative-upper-bound-left-factor-is-positive-mul-closed-interval-ℚ.
2 participants
Builds on #1688, #1689, and #1684.