truncatedSup_singleton — Mathlib

English

Let α be a semilattice with top. For any a, b ∈ α, the truncation of the singleton {b} at a is equal to b if a ≤ b, and is equal to ⊤ otherwise.

Русский

Пусть α — полупорядоченное множество с верхней границей, и b, a ∈ α. Усечение верхнего предела одиночки {b} над a равно b, если a ≤ b, иначе равно ⊤.

LaTeX

$$$\operatorname{truncatedSup}({b})\;a = \begin{cases} b, & a \le b \\ \top, & \text{иначе} \end{cases}$$$

Lean4

@[simp]
theorem truncatedSup_singleton (b a : α) : truncatedSup { b } a = if a ≤ b then b else ⊤ := by simp [truncatedSup];
  split_ifs <;> simp [Finset.filter_true_of_mem, *]

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