mulSupport_eq_iff — Mathlib

English

mulSupport f = s iff f is not equal to 1 on s and equals 1 outside s.

Русский

mulSupport f = s тогда и только тогда, когда f не равна 1 на s и равна 1 вне s.

LaTeX

$$$ \\mathrm{mulSupport}(f) = s \\iff \\big( \\forall x \\in s, f(x) \\neq 1 \\big) \\land \\big( \\forall x \\notin s, f(x) = 1 \\big) $$$

Lean4

@[to_additive]
theorem mulSupport_eq_iff : mulSupport f = s ↔ (∀ x, x ∈ s → f x ≠ 1) ∧ ∀ x, x ∉ s → f x = 1 := by
  simp +contextual only [Set.ext_iff, mem_mulSupport, ne_eq, iff_def, not_imp_comm, and_comm, forall_and]

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