IsDiscrete — Mathlib

English

There is an abbreviation IsDiscrete(X) for ContAction V G meaning that the underlying topology is discrete.

Русский

Существует аббревиатура IsDiscrete(X) для ContAction V G, означающая, что базовая топология дискретна.

LaTeX

$$$\\text{IsDiscrete }(X) := \\text{DiscreteTopology }((\\mathrm{forget}_2 \\; TopCat).obj X)$.$$

Lean4

/-- A predicate on an `X : ContAction V G` saying that the topology on the underlying type of `X`
is discrete. -/
abbrev IsDiscrete (X : ContAction V G) : Prop :=
  DiscreteTopology ((CategoryTheory.forget₂ _ TopCat).obj X)

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