IsCusp — Mathlib

English

Cusps of a subgroup 𝒢 of GL(2, R) are fixed points of parabolic elements of 𝒢.

Русский

Границы (куспы) подгруппы 𝒢 ⊆ GL(2, R) являются фиксированными точками параболических элементов 𝒢.

LaTeX

$$$$ \text{IsCusp}(c, \mathcal{G}) \;\iff\; \exists g \in \mathcal{G}: g \text{ is parabolic and } g \cdot c = c. $$$$

Lean4

/-- The *cusps* of a subgroup of `GL(2, ℝ)` are the fixed points of parabolic elements of `g`. -/
def IsCusp (c : OnePoint ℝ) (𝒢 : Subgroup (GL (Fin 2) ℝ)) : Prop :=
  ∃ g ∈ 𝒢, g.IsParabolic ∧ g • c = c

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