English
For a predicate P closed under ⊥ and ⊔, the supremum taken in the subtype {x | P x} coincides with the supremum taken in α of the underlying elements.
Русский
Пусть P — свойство, замкнутое относительно ⊥ и ⊔; супремум в подгруппе {x | P x} совпадает с супремумом в α для соответствующих оснований.
LaTeX
$$$\displaystyle \big( \sup t f \big) = t.\sup (\lambda x. (f x).1)$$$
Lean4
/-- Computing `sup` in a subtype (closed under `sup`) is the same as computing it in `α`. -/
theorem sup_coe {P : α → Prop} {Pbot : P ⊥} {Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)} (t : Finset β)
(f : β → { x : α // P x }) :
(@sup { x // P x } _ (Subtype.semilatticeSup Psup) (Subtype.orderBot Pbot) t f : α) = t.sup fun x => ↑(f x) :=
by
letI := Subtype.semilatticeSup Psup
letI := Subtype.orderBot Pbot
apply comp_sup_eq_sup_comp Subtype.val <;> intros <;> rfl
