topology.tactic

# 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.

@[continuity]
theorem continuous_id' {α : Type u_1}  :
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.

List of tactics used by continuity internally.

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

Version of continuity for use with auto_param.

continuity solves goals of the form continuous f by applying lemmas tagged with the continuity user attribute.

example {X Y : Type*} [topological_space X] [topological_space Y]
(f₁ f₂ : X → Y) (hf₁ : continuous f₁) (hf₂ : continuous f₂)
(g : Y → ℝ) (hg : continuous g) : continuous (λ x, (max (g (f₁ x)) (g (f₂ x))) + 1) :=
by continuity


will discharge the goal, generating a proof term like ((continuous.comp hg hf₁).max (continuous.comp hg hf₂)).add continuous_const

You can also use continuity!, which applies lemmas with { md := semireducible }. The default behaviour is more conservative, and only unfolds reducible definitions when attempting to match lemmas with the goal.

continuity? reports back the proof term it found.