Mathlib Map

Theorems · Theorem · order theory

StrictAnti.injective

∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → Function.Injective f
Defined in
Mathlib.Order.Monotone.Basic
Cited by
12 results in Mathlib
Foundations
Depth 18 from the axioms · uses propext, Quot.sound
Assumes
LinearOrderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasureTheory.Measure.addHaar_submodule · cited by 3Measure.addHaar_submoduleList.SortedGT.nodup · cited by 2SortedGT.noduppow_right_injective₀ · cited by 1pow_right_injective₀Set.isWF_iff_no_descending_seq · cited by 1Set.isWF_iff_no_descendin…zpow_right_injective₀ · cited by 1zpow_right_injective₀Real.rpow_right_inj · cited by 1Real.rpow_right_injStrictAnti.map_isGreatest · cited by 0StrictAnti.map_isGreatestStrictAnti.map_isLeast · cited by 0StrictAnti.map_isLeastAkraBazziRecurrence.injective_sumCoeffsExp · cited by 0AkraBazziRecurrence.injec…Subgroup.mem_closure_singleton_iff_existsUnique_zpow · cited by 0Subgroup.mem_closure_sing…AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul · cited by 0AddSubgroup.mem_closure_s…Antitone.strictAnti_iff_injective · cited by 0Antitone.strictAnti_iff_i…LinearOrder · cited by 8572LinearOrderPreorder · cited by 7952PreorderStrictAnti · cited by 204StrictAntiOrdering.Compares · cited by 31Ordering.ComparesStrictAnti.compares · cited by 1StrictAnti.comparesStrictAnti.injectiveCITED BYCITES

Cites5

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

Cited by12

Results whose statement or proof uses this declaration.