Theorems · Theorem · order theory

partialSups_iff_forall

∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  {f : ι → α} (p : α → Prop), (∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b) → ∀ {i : ι}, p ((partialSups f) i) ↔ ∀ j ≤ i, p (f j)

Defined in

Mathlib.Order.PartialSups

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemilatticeSupPreorderLocallyFiniteOrderBot