orbit_injective — Mathlib

English

If a and b represent the same quotient class modulo H, then they represent the same quotient class modulo G.

Русский

Если a и b эквивалентны по отношению к подгруппе H в фактор-множестве, то они эквивалентны по отношению к G.

LaTeX

$$$(\llbracket a \rrbracket : \text{orbitRel.Quotient } H\; \alpha) = (\llbracket b \rrbracket) \\Rightarrow (\llbracket a \rrbracket : \text{orbitRel.Quotient } G\; \alpha) = (\llbracket b \rrbracket)$$$

Lean4

@[to_additive]
theorem orbit_injective : Injective (orbitRel.Quotient.orbit : orbitRel.Quotient G α → Set α) :=
  by
  intro x y h
  simp_rw [orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq', orbit_eq_iff, ← orbitRel_apply] at h
  simpa [← Quotient.eq''] using h

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