sup'_inf_distrib_left — Mathlib

English

In a distributive lattice, a ⊓ s.sup' hs f = s.sup' hs (a ⊓ f i).

Русский

В распределительном сі-те решетке a ∧ (sup' s f) равно sup' hs (a ∧ f i).

LaTeX

$$$a \sqcap s.sup' hs f = s.sup' hs \bigl(\,a \sqcap f\bigr).$$$

Lean4

theorem sup'_inf_distrib_left (f : ι → α) (a : α) : a ⊓ s.sup' hs f = s.sup' hs fun i ↦ a ⊓ f i := by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp
  | cons _ _ _ hs ih => simp_rw [sup'_cons hs, inf_sup_left, ih]

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