support_eq — Mathlib

English

For a zero-start function f, its support equals the union of fibers over nonzero values.

Русский

Для функции f, начинающейся с нуля, поддержка равна объединению фибр над ненулевыми значениями.

LaTeX

$$$\\operatorname{support} f = \\bigcup_{y \\in \\{y \\in f.range \\mid y \\neq 0\\}} f^{-1}({y})$$$

Lean4

theorem support_eq [MeasurableSpace α] [Zero β] (f : α →ₛ β) : support f = ⋃ y ∈ {y ∈ f.range | y ≠ 0}, f ⁻¹' { y } :=
  Set.ext fun x => by
    simp only [mem_support, Set.mem_preimage, mem_filter, mem_range_self, true_and, exists_prop, mem_iUnion,
      mem_singleton_iff, exists_eq_right']

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