tacticBorelize___ — Mathlib

Lean4
/-- The behaviour of `borelize α` depends on the existing assumptions on `α`.

- if `α` is a topological space with instances `[MeasurableSpace α] [BorelSpace α]`, then
  `borelize α` replaces the former instance by `borel α`;
- otherwise, `borelize α` adds instances `borel α : MeasurableSpace α` and `⟨rfl⟩ : BorelSpace α`.

Finally, `borelize α β γ` runs `borelize α; borelize β; borelize γ`.
-/
@[tactic_parser 1000]
public meta def tacticBorelize___ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Borelize.tacticBorelize___ 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "borelize" false✝)
      (ParserDescr.unary✝ `many
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
          (ParserDescr.cat✝ `term 1024))))
Похожие утверждения