Theorems · Theorem · order theory

Set.eqOn_range

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_7} {f : ι → α} {g₁ g₂ : α → β},
  Set.EqOn g₁ g₂ (Set.range f) ↔ g₁ ∘ f = g₂ ∘ f

Defined in

Mathlib.Data.Set.Function

Cited by

4 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Quot.sound