partialSups_bot — Mathlib

English

If ι has a bottom element and α has a semilattice structure, then partialSups f ⊥ = f ⊥.

Русский

Если в ι есть ноль (нижняя граница) и α имеет структуру полуупорядочения, то partialSups f ⊥ = f ⊥.

LaTeX

$$$\\partialSups f \\; \\bot = f \\; \\bot$$$

Lean4

@[simp]
theorem partialSups_bot [PartialOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] (f : ι → α) : partialSups f ⊥ = f ⊥ :=
  by
  simp only [partialSups_apply]
    -- should we add a lemma `Finset.Iic_bot`?

  suffices Iic (⊥ : ι) = {⊥} by simp only [this, sup'_singleton]
  simp only [← coe_eq_singleton, coe_Iic, Set.Iic_bot]

Похожие утверждения