truncatedSup_infs_of_notMem — Mathlib

English

If a ∉ lowerClosure s ⊓ lowerClosure t, then truncatedSup (s ⊻ t) a equals ⊤.

Русский

Если a ∉ нижнее замыкание s ⊓ t, тогда truncatedSup(s ⊻ t) a = ⊤.

LaTeX

$$$a \notin \operatorname{lowerClosure}(s) \sqcap \operatorname{lowerClosure}(t) \Rightarrow \operatorname{truncatedSup}(s \odot t) \, a = \top$$$

Lean4

theorem truncatedSup_infs_of_notMem (ha : a ∉ lowerClosure s ⊓ lowerClosure t) : truncatedSup (s ⊼ t) a = ⊤ :=
  truncatedSup_of_notMem <| by rwa [coe_infs, lowerClosure_infs]

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