isContinuous_def — Mathlib

English

The is-continuous predicate for an action X is equivalent to the explicit continuity of the action map: the map from G × |X| to |X| given by p ↦ ρ_{p.1}(p.2) is continuous.

Русский

Предикат непрерывности действия X эквивалентен явному требованию непрерывности отображения действия: отображение (g, x) ↦ ρ_g(x) непрерывно.

LaTeX

$$$X.IsContinuous \\iff \\; Continuous\\Bigl(\\lambda p : G \\times ((\\mathrm{forget}_2\\,TopCat).obj X) \\mapsto (\\mathrm{forget}_2\\,TopCat).map (X.\\rho\\ p.1) p.2\\Bigr).$$$

Lean4

theorem isContinuous_def (X : Action V G) :
    X.IsContinuous ↔ Continuous (fun p : G × (forget₂ _ TopCat).obj X ↦ (forget₂ _ TopCat).map (X.ρ p.1) p.2) :=
  ⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩

Похожие утверждения