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 := reducible) :
list (tactic string)

List of tactics used by continuity internally.

source
meta def tactic.interactive.continuity (bang : interactive.parse (lean.parser.tk "!")?) (trace : interactive.parse (lean.parser.tk "?")?) (cfg : tactic.tidy.cfg := {trace_result := 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.