truncatedInf_singleton — Mathlib

English

For a singleton {b}, truncatedInf {b} a equals b if b ≤ a and equals ⊥ otherwise.

Русский

Для одиночного множества {b} truncInf {b} a = b если b ≤ a, иначе ⊥.

LaTeX

$$$\operatorname{truncatedInf} \{b\} \, a = \begin{cases} b, & b \le a \\ \bot, & \text{иначе} \end{cases}$$$

Lean4

@[simp]
theorem truncatedInf_singleton (b a : α) : truncatedInf { b } a = if b ≤ a then b else ⊥ :=
  by
  simp only [truncatedInf, coe_singleton, upperClosure_singleton, UpperSet.mem_Ici_iff, id_eq]
  split_ifs <;> simp [Finset.filter_true_of_mem, *]

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