group_inseparable_iff — Mathlib

English

For any x,y in G, x and y are inseparable iff x/y lies in the closure of {1}.

Русский

Для любых x,y в G, x и y неразделимы тогда и только тогда, когда x/y принадлежит замыканию множества {1}.

LaTeX

$$$\\operatorname{Inseparable}(x,y) \\iff x / y \\in \\overline{\\{1\\}}$$$

Lean4

@[to_additive]
theorem group_inseparable_iff {x y : G} : Inseparable x y ↔ x / y ∈ closure (1 : Set G) :=
  by
  rw [← singleton_one, ← specializes_iff_mem_closure, specializes_comm, specializes_iff_inseparable, ←
    (Homeomorph.mulRight y⁻¹).isEmbedding.inseparable_iff]
  simp [div_eq_mul_inv]

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