truncatedInf_le — Mathlib

English

Under suitable distributive lattice structure, the truncatedInf of s ⊼ t at a equals the infimum of truncatedInf s a and truncatedInf t a.

Русский

В распределимой решётке для s ⊼ t выполняется truncatedInf(s ⊼ t) a = truncatedInf s a ⊓ truncatedInf t a.

LaTeX

$$$\operatorname{truncatedInf}(s \; \sqcap \; t) \, a = \operatorname{truncatedInf} s \, a \sqcap \operatorname{truncatedInf} t \, a$$$

Lean4

theorem truncatedInf_le : truncatedInf s a ≤ a := by
  unfold truncatedInf
  split_ifs with h
  · obtain ⟨b, hb, hba⟩ := h
    exact hba.trans' <| inf'_le id <| mem_filter.2 ⟨hb, ‹_›⟩
  · exact bot_le

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