disjoint_smul_set_left — Mathlib

English

Let a act on set s by left multiplication. Then for any two subsets s and t of the group-acted space, Disjoint(a • s, t) holds if and only if Disjoint(s, a⁻¹ • t).

Русский

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

LaTeX

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

Lean4

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

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