Mathlib Map

Theorems · Theorem · logic and foundations

Set.ofPred_subset_ofPred

∀ {α : Type u} {p q : α → Prop}, {a | p a} ⊆ {a | q a} ↔ ∀ (a : α), p a → q a
Defined in
Mathlib.Data.Set.Basic
Cited by
3 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.ofPred_subset_ofPred_of_imp · cited by 22Set.ofPred_subset_ofPred_…ZSpan.fundamentalDomain_subset_parallelepiped · cited by 1ZSpan.fundamentalDomain_s…Set.setOf_subset_setOf · cited by 0Set.setOf_subset_setOfSet · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredSet.ofPred_subset_ofPredCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Set.ofPredstatement · cited by 6,101

Cited by3

Results whose statement or proof uses this declaration.