mem_fundamentalFrontier — Mathlib

English

A point x lies in the frontier of the fundamental domain precisely when x belongs to the domain and there exists a nontrivial group element g with x ∈ g·s.

Русский

Точка x принадлежит границе фундаментальной области тогда и только тогда, когда она принадлежит области и существует ненулевой элемент группы g с x ∈ g·s.

LaTeX

$$$x \\in \\mathrm{fundamentalFrontier}(G,s) \\;\\iff\\; x \\in s \\;\\land\\; \\exists g \\in G, g \\neq 1 \\land x \\in g \\cdot s$$$

Lean4

@[to_additive (attr := simp) MeasureTheory.mem_addFundamentalFrontier]
theorem mem_fundamentalFrontier : x ∈ fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g : G, g ≠ 1 ∧ x ∈ g • s := by
  simp [fundamentalFrontier]

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