Theorems · Theorem · order theory

Finset.filter_infs_le

∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] [inst_2 : DecidableLE α] (s t : Finset α) (a : α),
  {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}

Defined in

Mathlib.Data.Finset.Sups

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqSemilatticeInfDecidableLE