prod_bot_sup_bot_prod — Mathlib

English

For subsemirings s ⊆ R and t ⊆ S, s.prod ⊥ ⊔ prod ⊥ t = s.prod t.

Русский

Для подпол semiring s и t верно: s.prod ⊥ ⊔ prod ⊥ t = s.prod t.

LaTeX

$$$s.prod\\bot \\uplus (\\bot.prod t) = s.prod t$$$

Lean4

@[simp]
theorem prod_bot_sup_bot_prod (s : Subsemiring R) (t : Subsemiring S) : s.prod ⊥ ⊔ prod ⊥ t = s.prod t :=
  le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) fun p hp =>
    Prod.fst_mul_snd p ▸
      mul_mem ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, SetLike.mem_coe.2 <| one_mem ⊥⟩)
        ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨SetLike.mem_coe.2 <| one_mem ⊥, hp.2⟩)

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