orbitRel_le_fst — Mathlib

English

The orbit relation on a product α × β is contained in the comap under the first projection of the orbit relation on α.

Русский

Орбитальная связь на произведении α × β содержится в обратном образе по проекции на первый фактор орбитальной связи на α.

LaTeX

$$orbitRel G (α × β) ≤ (orbitRel G α).comap Prod.fst$$

Lean4

@[to_additive]
theorem orbitRel_le_fst : orbitRel G (α × β) ≤ (orbitRel G α).comap Prod.fst :=
  Setoid.le_def.2 fst_mem_orbit_of_mem_orbit

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