Theorems · Theorem · general topology

range_eq_image_tsupport_or

∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] (f : X → α),
  Set.range f = f '' tsupport f ∨ Set.range f = insert 0 (f '' tsupport f)

Defined in

Mathlib.Topology.Algebra.Support

Cited by

0 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ZeroTopologicalSpace