Theorems · Theorem · order theory
DirectedOn.directed_val
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, DirectedOn r s → Directed r Subtype.valAlias of the forward direction of directedOn_iff_directed.
- Defined in
- Mathlib.Order.Directed
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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 · cited by 271
- Directedstatement · cited by 213
- directedOn_iff_directedproof · cited by 14
Cited by36
Results whose statement or proof uses this declaration.
- Submodule.mem_sSup_of_directedproof · cited by 6
- Filter.mem_biInf_of_directedproof · cited by 5
- DirectedOn.exists_mem_subset_of_finset_subset_biUnionproof · cited by 3
- Set.pairwise_sUnionproof · cited by 3
- IntermediateField.adjoin_simple_isCompactElementproof · cited by 2
- exists_idempotent_of_compact_t2_of_continuous_add_leftproof · cited by 2
- exists_idempotent_of_compact_t2_of_continuous_mul_leftproof · cited by 2
- Subfield.mem_sSup_of_directedOnproof · cited by 1
- orthonormal_sUnion_of_directedproof · cited by 1
- AddSubmonoid.mem_sSup_of_directedOnproof · cited by 1
- NonUnitalSubsemiring.mem_sSup_of_directedOnproof · cited by 1
- Subsemigroup.mem_sSup_of_directed_onproof · cited by 1