truncatedInf — Mathlib

English

If e is an order isomorphism, then e(truncatedInf s a) equals truncatedInf of the image of s at e(a).

Русский

Пусть e — отображение-изоморфизм порядка. Тогда e(truncatedInf s a) = truncatedInf (map s) (e a).

LaTeX

$$$e\bigl(\operatorname{truncatedInf} s \, a\bigr) = \operatorname{truncatedInf}\bigl( s.map e.toEquiv.toEmbedding \bigr) (e a)$$$

Lean4

/-- The infimum of the elements of `s` less than `a` if there are some, otherwise `⊥`. -/
def truncatedInf (s : Finset α) (a : α) : α :=
  if h : a ∈ upperClosure s then {b ∈ s | b ≤ a}.inf' (inf_aux h) id else ⊥

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