Mathlib Map

Theorems · Theorem · order theory

Set.LeftInvOn.eqOn

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f' : β → α}, Set.LeftInvOn f' f s → Set.EqOn (f' ∘ f) id s
Defined in
Mathlib.Data.Set.Function
Cited by
3 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

OpenPartialHomeomorph.map_extend_symm_nhdsWithin · cited by 4OpenPartialHomeomorph.map…CStarAlgebra.directedOn_nonneg_ball · cited by 1CStarAlgebra.directedOn_n…ModelWithCorners.isInvertible_fderivWithin_extendCoordChange · cited by 1ModelWithCorners.isInvert…Set · cited by 53352SetSet.EqOn · cited by 603Set.EqOnSet.LeftInvOn · cited by 42Set.LeftInvOnLeftInvOn.eqOnCITED BYCITES

Cites3

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.EqOnstatement · cited by 603
  • Set.LeftInvOnstatement and proof · cited by 42

Cited by3

Results whose statement or proof uses this declaration.