Theorems · Theorem · order theory
DirectedOn.mono
∀ {α : Type u_1} {r r' : α → α → Prop} {s : Set α}, DirectedOn r s → (∀ ⦃a b : α⦄, r a b → r' a b) → DirectedOn r' s- Defined in
- Mathlib.Order.Directed
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- DirectedOnstatement and proof · cited by 271
- DirectedOn.mono'proof · cited by 1
Cited by8
Results whose statement or proof uses this declaration.
- DirectedOn.mono_compproof · cited by 10
- exists_sSupIndep_disjoint_sSup_atomsproof · cited by 2
- Topology.IsScott.scottContinuousOn_iff_continuousproof · cited by 2
- DirectedOn.fstproof · cited by 1
- UniformOnFun.hasBasis_uniformity_of_basis_aux₂proof · cited by 1
- RieszExtension.exists_topproof · cited by 1
- DirectedOn.sndproof · cited by 1
- DirectedOn.projproof · cited by 0