Theorems · Theorem · order theory

Set.MapsTo.restrict_inj

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : Set.MapsTo f s t),
  Function.Injective (Set.MapsTo.restrict f s t h) ↔ Set.InjOn f s

Defined in: Mathlib.Data.Set.Restrict
Cited by: 4 results in Mathlib
Foundations: Depth 10 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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.Elemstatement and proof · cited by 7,166
Set.MapsTostatement and proof · cited by 732
Set.InjOnstatement and proof · cited by 543
Set.domRestrictproof · cited by 383
Set.MapsTo.restrictstatement · cited by 57
Set.injOn_iff_injectiveproof · cited by 20
Set.injective_codRestrictproof · cited by 10
Set.MapsTo.restrict_eq_codRestrictproof · cited by 1

Cited by4

Results whose statement or proof uses this declaration.

DiscreteTopology.preimage_of_continuous_injectiveproof · cited by 1
Set.exists_ne_map_eq_of_encard_lt_of_maps_toproof · cited by 1
Set.Finite.injOn_iff_bijOn_of_mapsToproof · cited by 1
Set.Finite.surjOn_iff_bijOn_of_mapsToproof · cited by 0