prod_bot_sup_bot_prod — Mathlib

English

In the product of two rings, the join of the bottom subring copies equals the full product: (s × 0) ⊔ (0 × t) = s × t.

Русский

В произведении колец соединение двух подкольц-образов (s × 0) ⊔ (0 × t) дает полный произведение s × t.

LaTeX

$$$ (s. prod \\; \\bot) \\lor (\\bot. prod \\; t) = s. prod t $$$

Lean4

@[simp]
theorem prod_bot_sup_bot_prod (s : Subring R) (t : Subring 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⟩)

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