pairwise_disjoint_fundamentalInterior

English

The family {g·fundamentalInterior(G,s) : g ∈ G} is pairwise disjoint; any two distinct translates do not intersect.

Русский

Семейство {g·fundamentalInterior(G,s) : g ∈ G} парно непересекаемо; любые две разные транспозиции не пересекаются.

LaTeX

$$Pairwise Disjoint on fun g : G => g · fundamentalInterior(G,s)$$

Lean4

@[to_additive MeasureTheory.pairwise_disjoint_addFundamentalInterior]
theorem pairwise_disjoint_fundamentalInterior : Pairwise (Disjoint on fun g : G => g • fundamentalInterior G s) :=
  by
  refine fun a b hab => disjoint_left.2 ?_
  rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩
  rw [mem_fundamentalInterior] at hx hy
  refine hx.2 (a⁻¹ * b) ?_ ?_
  · rwa [Ne, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
  · simpa [mul_smul, ← hxy, mem_inv_smul_set_iff] using hy.1

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