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).
```

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

Last updated: May 28 2024 at 08:21 UTC