Mathlib Map

Theorems · Theorem · order theory

subset_rfl

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

Set notation form of le_rfl

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

Around this declaration

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

Matroid.IsBase.indep · cited by 22IsBase.indepUniformFun.hasBasis_uniformity_of_basis · cited by 8UniformFun.hasBasis_unifo…MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le · cited by 7MeasureTheory.isTightMeas…isSeparatedMap_iff_isClosed_diagonal · cited by 4isSeparatedMap_iff_isClos…IsUltraUniformity.mk_of_hasBasis · cited by 4IsUltraUniformity.mk_of_h…IsLinearTopology.mk_of_hasBasis' · cited by 4IsLinearTopology.mk_of_ha…isClosedMap_iff_comap_nhdsSet_le · cited by 3isClosedMap_iff_comap_nhd…IsMIntegralCurveOn.comp_add · cited by 3IsMIntegralCurveOn.comp_a…IsMIntegralCurveOn.comp_mul · cited by 3IsMIntegralCurveOn.comp_m…locallyConnectedSpace_of_connected_bases · cited by 3locallyConnectedSpace_of_…AntilipschitzWith.isBounded_of_image2_left · cited by 3AntilipschitzWith.isBound…Infinite.exists_superset_card_eq · cited by 3Infinite.exists_superset_…Topology.RelCWComplex.Subcomplex.subset_complex · cited by 3Subcomplex.subset_complexIsLinearTopology.hasBasis_twoSidedIdeal · cited by 3IsLinearTopology.hasBasis…IsClosedMap.isEvenlyCovered_of_openPartialHomeomorph · cited by 2IsClosedMap.isEvenlyCover…Preorder · cited by 7952Preorderle_rfl · cited by 1558le_rflsubset_rflCITED 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
  • le_rflproof · cited by 1,558

Cited by77

Results whose statement or proof uses this declaration.