Stream: SErAPIS

Topic: intermediate value theorem

view this post on Zulip Wenda Li (May 14 2021 at 21:05):

One data point: I intended to search for the intermediate value theorem in the standard library, given the concept 'topology' or 'real analysis', but SErAPIs appeared to have a hard time on this query. My expected answers are 

Topological_Spaces.IVT:
    ?f ?a ≤ ?y ⟹
    ?y ≤ ?f ?b ⟹ ?a ≤ ?b ⟹ ∀x. ?a ≤ x ∧ x ≤ ?b ⟶ isCont ?f x ⟹ ∃x≥?a. x ≤ ?b ∧ ?f x = ?y

and

  Limits.IVT_objl:
    ?f ?a ≤ ?y ∧ ?y ≤ ?f ?b ∧ ?a ≤ ?b ∧ (∀x. ?a ≤ x ∧ x ≤ ?b ⟶ isCont ?f x) ⟶
    (∃x≥?a. x ≤ ?b ∧ ?f x = ?y).

view this post on Zulip Notification Bot (May 21 2021 at 11:31):

This topic was moved here from #alexandria > SEraPIS by Anthony Bordg

Last updated: Apr 19 2024 at 20:15 UTC