truncatedInf_of_mem — Mathlib

English

If a ∈ upperClosure s, then truncatedInf s a equals the infimum of {b ∈ s | b ≤ a} in the appropriate infimum structure.

Русский

Если a ∈ верхнееClosure s, то truncatedInf s a равно наибольшему нижнему пределу множества {b ∈ s | b ≤ a}.

LaTeX

$$$a \in \operatorname{upperClosure}(s) \Rightarrow \operatorname{truncatedInf} \; s \; a = \inf'\{b \in s \mid b \le a\} (\text{id})$$$

Lean4

theorem truncatedInf_of_mem (h : a ∈ upperClosure s) : truncatedInf s a = {b ∈ s | b ≤ a}.inf' (inf_aux h) id :=
  dif_pos h

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