orbitRel_le_snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem orbitRel_le_snd : orbitRel G (α × β) ≤ (orbitRel G β).comap Prod.snd :=
  Setoid.le_def.2 snd_mem_orbit_of_mem_orbit

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