Mathlib Map

Theorems · Definition · order theory

Set.dissipate

{α : Type u_1} → {β : Type u_2} → [LE α] → (α → Set β) → α → Set β

dissipate s is the intersection of s y for y ≤ x.

Defined in
Mathlib.Order.SetDissipate
Cited by
24 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
LE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsCompactSystem · cited by 15IsCompactSystemSet.antitone_dissipate · cited by 4Set.antitone_dissipateIsCompactSystem.insert_univ · cited by 2IsCompactSystem.insert_un…IsCompactSystem.of_nonempty_iInter · cited by 2IsCompactSystem.of_nonemp…isCompactSystem_isCompact_isClosed · cited by 2isCompactSystem_isCompact…Set.dissipate_subset · cited by 2Set.dissipate_subsetSet.dissipate_succ · cited by 2Set.dissipate_succSet.dissipate_zero_nat · cited by 2Set.dissipate_zero_natSet.exists_dissipate_eq_empty_iff_of_directed · cited by 1Set.exists_dissipate_eq_e…Set.iInter_dissipate · cited by 1Set.iInter_dissipateIsCompactSystem.iff_nonempty_iInter · cited by 1IsCompactSystem.iff_nonem…IsCompactSystem.nonempty_iInter · cited by 1IsCompactSystem.nonempty_…isCompactSystem_iff_of_directed · cited by 1isCompactSystem_iff_of_di…IsPiSystem.dissipate_mem · cited by 1IsPiSystem.dissipate_memSet.dissipate_eq_biInter_lt · cited by 1Set.dissipate_eq_biInter_…Set · cited by 53352SetSet.iInter · cited by 1084Set.iInterSet.dissipateCITED BYCITES

Cites2

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
  • Set.iInterproof · cited by 1,084

Cited by25

Results whose statement or proof uses this declaration.