Mathlib Map

Theorems · Theorem · order theory

Finset.fold_inf_univ

∀ {α : Type u_2} [inst : Fintype α] [inst_1 : SemilatticeInf α] [inst_2 : OrderBot α] (a : α),
  Finset.fold min a (fun x => x) Finset.univ = ⊥
Defined in
Mathlib.Data.Fintype.Lattice
Cited by
1 results in Mathlib
Foundations
Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FintypeSemilatticeInfOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.fold_sup_univ · cited by 0Finset.fold_sup_univFintype · cited by 7736FintypeBot.bot · cited by 4720Bot.botFinset.univ · cited by 3473Finset.univle_rfl · cited by 1558le_rflOrderBot · cited by 1055OrderBotSemilatticeInf · cited by 634SemilatticeInfFinset.mem_univ · cited by 361Finset.mem_univeq_bot_iff · cited by 159eq_bot_iffle_inf_iff · cited by 48le_inf_iffFinset.fold · cited by 46Finset.foldFinset.fold_op_rel_iff_and · cited by 5Finset.fold_op_rel_iff_andFinset.fold_inf_univCITED BYCITES

Cites11

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

Cited by1

Results whose statement or proof uses this declaration.