Mathlib Map

Theorems · Theorem · order theory

IsLowerSet.preimage

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
  IsLowerSet s → ∀ {f : β → α}, Monotone f → IsLowerSet (f ⁻¹' s)
Defined in
Mathlib.Order.UpperLower.Basic
Cited by
3 results in Mathlib
Foundations
Depth 5 from the axioms · uses propext
Assumes
PreorderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsLowerSet.image · cited by 2IsLowerSet.imageOrder.IsNormal.continuous · cited by 1IsNormal.continuousStableUnderSpecialization.preimage · cited by 0StableUnderSpecialization…Set · cited by 53352SetPreorder · cited by 7952PreorderSet.preimage · cited by 4946Set.preimageMonotone · cited by 1397MonotoneIsLowerSet · cited by 167IsLowerSetIsLowerSet.preimageCITED BYCITES

Cites5

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
  • Preorderstatement and proof · cited by 7,952
  • Set.preimagestatement · cited by 4,946
  • Monotonestatement and proof · cited by 1,397
  • IsLowerSetstatement and proof · cited by 167

Cited by3

Results whose statement or proof uses this declaration.