mathlib documentation


Tactics for topology #

Currently we have one domain-specific tactic for topology: continuity.

continuity tactic #

Automatically solve goals of the form continuous f.

Mark lemmas with @[continuity] to add them to the set of lemmas used by continuity.

meta def continuity  :

User attribute used to mark tactics used by continuity.

theorem continuous_id' {α : Type u_1} [topological_space α] :
continuous (λ (a : α), a)

Tactic to apply continuous.comp when appropriate.

Applying continuous.comp is not always a good idea, so we have some extra logic here to try to avoid bad cases.

  • If the function we're trying to prove continuous is actually constant, and that constant is a function application f z, then continuous.comp would produce new goals continuous f, continuous (λ _, z), which is silly. We avoid this by failing if we could apply continuous_const.

  • continuous.comp will always succeed on continuous (λ x, f x) and produce new goals continuous (λ x, x), continuous f. We detect this by failing if a new goal can be closed by applying continuous_id.

Solve goals of the form continuous f. continuity? reports back the proof term it found.

Version of continuity for use with auto_param.