mathlib documentation

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.

source
meta def continuity  :
(user_attribute unit)

User attribute used to mark tactics used by continuity.

source
@[continuity]
theorem continuous_id' {α : Type u_1} [topological_space α] :
continuous (λ (a : α), a)
source
meta def tactic.apply_continuous.comp  :
tactic unit

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.

source
meta def tactic.continuity_tactics (md : tactic.transparency := tactic.transparency.reducible) :
list (tactic string)

List of tactics used by continuity internally.

source
meta def tactic.interactive.continuity (bang : interactive.parse (optional (lean.parser.tk "!"))) (trace : interactive.parse (optional (lean.parser.tk "?"))) (cfg : tactic.tidy.cfg := {trace_result := bool.ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) :
tactic unit

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

source
meta def tactic.interactive.continuity'  :
tactic unit

Version of continuity for use with auto_param.

source
def tactic_doc.tactic.continuity / continuity'  :
tactic_doc_entry

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.