Mathlib Map

Theorems · Theorem · order theory

IsUpperSet.preimage

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

Around this declaration

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

IsUpperSet.image · cited by 2IsUpperSet.imageTopology.IsScott.scottContinuousOn_iff_continuous · cited by 2IsScott.scottContinuousOn…MvPolynomial.idealOfVars_eq_restrictSupportIdeal · cited by 1MvPolynomial.idealOfVars_…MvPolynomial.pow_idealOfVars · cited by 1MvPolynomial.pow_idealOfV…Topology.IsUpperSet.monotone_iff_continuous · cited by 1IsUpperSet.monotone_iff_c…Topology.IsUpperSet.monotone_to_upperTopology_continuous · cited by 1IsUpperSet.monotone_to_up…MvPolynomial.mem_pow_idealOfVars_iff · cited by 0MvPolynomial.mem_pow_idea…StableUnderGeneralization.preimage · cited by 0StableUnderGeneralization…Set · cited by 53352SetPreorder · cited by 7952PreorderSet.preimage · cited by 4946Set.preimageMonotone · cited by 1397MonotoneIsUpperSet · cited by 148IsUpperSetIsUpperSet.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
  • IsUpperSetstatement and proof · cited by 148

Cited by8

Results whose statement or proof uses this declaration.