mulSupport_nonempty_iff — Mathlib

English

For any function f: ι → M, the set { i ∈ ι | f(i) ≠ 1 } is nonempty if and only if f is not identically equal to the unit element 1.

Русский

Для произвольной функции f: ι → M множество { i ∈ ι | f(i) ≠ 1 } непусто тогда и только тогда, когда f не тождественно равно единице.

LaTeX

$$$ (\operatorname{mulSupport} f) \neq \emptyset \iff f \neq 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem mulSupport_nonempty_iff : (mulSupport f).Nonempty ↔ f ≠ 1 := by
  rw [nonempty_iff_ne_empty, Ne, mulSupport_eq_empty_iff]

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