disjoint_smul_set_right — Mathlib

English

Let a act on set t by right translation. Then Disjoint(s, a • t) holds iff Disjoint(a⁻¹ • s, t).

Русский

Пусть элемент группы действует справа на множество T; тогда Disjoint(S, a • T) эквивалентно Disjoint(a⁻¹ • S, T).

LaTeX

$$$\\operatorname{Disjoint}(S, a \\cdot T) \\iff \\operatorname{Disjoint}(a^{-1} \\cdot S, T)$$$

Lean4

@[to_additive]
theorem disjoint_smul_set_right : Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t := by
  simpa using disjoint_smul_set (a := a) (s := a⁻¹ • s)

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