truncatedInf_sups_of_notMem — Mathlib

English

If a ∉ upperClosure s ⊔ upperClosure t, then truncatedInf (s ⊻ t) a = ⊤.

Русский

Если a не в верхнем замыкании s ⊔ t, тогда truncatedInf(s ⊻ t) a = ⊤.

LaTeX

$$$a \notin \operatorname{upperClosure}(s) \sqcup \operatorname{upperClosure}(t) \Rightarrow \operatorname{truncatedInf}(s \odot t) \, a = \top$$$

Lean4

theorem truncatedInf_sups_of_notMem (ha : a ∉ upperClosure s ⊔ upperClosure t) : truncatedInf (s ⊻ t) a = ⊥ :=
  truncatedInf_of_notMem <| by rwa [coe_sups, upperClosure_sups]

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