disjoint_conj — Mathlib

English

If Disjoint f g, then Disjoint (h f h^{-1}) (h g h^{-1}) for any h.

Русский

Если Disjoint f g, то Disjoint (h f h^{-1}) (h g h^{-1}) при любом h.

LaTeX

$$$\forall h:\operatorname{Perm}(\alpha),\ \operatorname{Disjoint}(f,g) \Rightarrow \operatorname{Disjoint}(h f h^{-1},\; h g h^{-1})$$$

Lean4

@[simp]
theorem disjoint_conj (h : Perm α) : Disjoint (h * f * h⁻¹) (h * g * h⁻¹) ↔ Disjoint f g :=
  (h⁻¹).forall_congr fun {_} ↦ by simp only [mul_apply, eq_inv_iff_eq]

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