Theorems · Theorem · general algebraic systems

Function.range_eq_image_or_of_support_subset

∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {k : Set ι},
  Function.support f ⊆ k → Set.range f = f '' k ∨ Set.range f = insert 0 (f '' k)

Defined in: Mathlib.Algebra.Notation.Support
Cited by: 1 results in Mathlib
Foundations: Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Zero

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.imagestatement and proof · cited by 5,609
Set.rangestatement and proof · cited by 4,705
LE.le.transproof · cited by 3,151
Function.supportstatement and proof · cited by 610
Set.image_monoproof · cited by 197
Set.insert_subset_insertproof · cited by 18
Function.range_subset_insert_image_supportproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

isCompact_range_of_support_subset_isCompactproof · cited by 2