mem_support_swap_mul_imp_mem_support_ne

English

If y lies in the support of swap x (f x) ⋅ f, then y belongs to the support of f and y ≠ x.

Русский

Если y лежит в опоре swap x (f x) ⋅ f, то y ∈ supp(f) и y ≠ x.

LaTeX

$$$\text{If } y \in \operatorname{supp}(\operatorname{swap} x (f x) \cdot f), \text{ then } y \in \operatorname{supp}(f) \land y \neq x.$$$

Lean4

theorem mem_support_swap_mul_imp_mem_support_ne {x y : α} (hy : y ∈ support (swap x (f x) * f)) :
    y ∈ support f ∧ y ≠ x :=
  by
  simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *
  grind

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