coe_sup — Mathlib

English

The underlying set of the supremum equals the union of underlying sets.

Русский

Подмножество верхнего элемента равняется объединению подмножеств.

LaTeX

$$$$ ((s ⊔ t : L.DefinableSet A α) : Set(α \\to M)) = (s : Set(α \\to M)) \\cup (t : Set(α \\to M)). $$$$

Lean4

@[simp, norm_cast]
theorem coe_sup (s t : L.DefinableSet A α) :
    ((s ⊔ t : L.DefinableSet A α) : Set (α → M)) = (s : Set (α → M)) ∪ (t : Set (α → M)) :=
  rfl

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