disjoint_refl_iff — Mathlib

English

A permutation is disjoint with itself if and only if it is the identity.

Русский

Перестановка раздельна с самой собой тогда и только тогда, когда она тождественна.

LaTeX

$$$\operatorname{Disjoint}(f,f) \iff f = 1$$$

Lean4

@[simp]
theorem disjoint_refl_iff : Disjoint f f ↔ f = 1 :=
  by
  refine ⟨fun h => ?_, fun h => h.symm ▸ disjoint_one_left 1⟩
  ext x
  rcases h x with hx | hx <;> simp [hx]

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