Mathlib Map

Theorems · Theorem · order theory

Set.InvOn.symm

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.InvOn f' f s t → Set.InvOn f f' t s
Defined in
Mathlib.Data.Set.Function
Cited by
2 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Nat.bijOn_digitsAppend · cited by 1Nat.bijOn_digitsAppendSet.bijOn_comm · cited by 1Set.bijOn_commSet · cited by 53352SetSet.InvOn · cited by 26Set.InvOnInvOn.symmCITED BYCITES

Cites2

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.InvOnstatement and proof · cited by 26

Cited by2

Results whose statement or proof uses this declaration.