Mathlib Map

Theorems · Theorem · order theory

Subtype.mono_coe

∀ {α : Type u} [inst : Preorder α] (p : α → Prop), Monotone Subtype.val
Defined in
Mathlib.Order.Monotone.Defs
Cited by
15 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Filter.map_val_atBot_of_Iic_subset · cited by 3Filter.map_val_atBot_of_I…Filter.map_val_atTop_of_Ici_subset · cited by 3Filter.map_val_atTop_of_I…FirstOrder.Language.equiv_between_cg · cited by 2Language.equiv_between_cgMeasureTheory.Measure.ext_of_Iic · cited by 2Measure.ext_of_IicIsCofinal.trans · cited by 2IsCofinal.transReal.monotone_arcsin · cited by 2Real.monotone_arcsinSet.image_subtype_val_uIcc · cited by 1Set.image_subtype_val_uIccSet.image_subtype_val_uIoc · cited by 1Set.image_subtype_val_uIocSet.image_subtype_val_uIoo · cited by 1Set.image_subtype_val_uIooFirstOrder.Language.embedding_from_cg · cited by 0Language.embedding_from_cgsInf_within_of_ordConnected · cited by 0sInf_within_of_ordConnect…Equiv.image_antitone · cited by 0Equiv.image_antitoneField.Emb.Cardinal.directed_filtration · cited by 0Cardinal.directed_filtrat…sSup_within_of_ordConnected · cited by 0sSup_within_of_ordConnect…Equiv.image_monotone · cited by 0Equiv.image_monotonePreorder · cited by 7952PreorderMonotone · cited by 1397MonotoneSubtype.mono_coeCITED BYCITES

Cites2

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

  • Preorderstatement and proof · cited by 7,952
  • Monotonestatement · cited by 1,397

Cited by15

Results whose statement or proof uses this declaration.