Mathlib Map

Theorems · Theorem · order theory

Eq.superset

∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a = b → b ⊆ a

Set notation form of Eq.ge

Defined in
Mathlib.Order.RelClasses
Cited by
16 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
UsesSetNotationForOrderPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Graph.Compatible.ext · cited by 9Compatible.extIsLocalHomeomorphOn.discreteTopology_of_image · cited by 3IsLocalHomeomorphOn.discr…PartitionOfUnity.sum_finsupport · cited by 2PartitionOfUnity.sum_fins…totallySeparatedSpace_of_t0_of_basis_clopen · cited by 2totallySeparatedSpace_of_…Set.singleton_ne_univ · cited by 2Set.singleton_ne_univbalancedCore_nonempty_iff · cited by 2balancedCore_nonempty_iffSubgroup.exists_finiteIndex_of_leftCoset_cover_aux · cited by 2Subgroup.exists_finiteInd…AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux · cited by 2AddSubgroup.exists_finite…Real.Convex.dimH_eq_finrank_vectorSpan · cited by 1Convex.dimH_eq_finrank_ve…Set.Ioc_eq_Ioc_iff · cited by 1Set.Ioc_eq_Ioc_iffSubmodule.map_covBy_of_injective · cited by 1Submodule.map_covBy_of_in…IsClosed.intrinsicClosure · cited by 1IsClosed.intrinsicClosureHasCompactSupport.tsupport_extend_zero · cited by 0HasCompactSupport.tsuppor…Set.Ico_eq_Ico_iff · cited by 0Set.Ico_eq_Ico_iffPairwise.biUnion_injective · cited by 0Pairwise.biUnion_injectivePreorder · cited by 7952PreorderEq.ge · cited by 375Eq.geEq.supersetCITED 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
  • Eq.geproof · cited by 375

Cited by16

Results whose statement or proof uses this declaration.