prod_bot_sup_bot_prod — Mathlib

English

If f is a monoid equivalence, then the image of K under f equals the comap of K.symm under f.symm.

Русский

Если f — эквив моноидов, то образ K под f равен обратному образу K.symm по f.symm.

LaTeX

$$$ K.map f = K.comap f.symm. $$$

Lean4

@[to_additive (attr := simp) prod_bot_sup_bot_prod]
theorem prod_bot_sup_bot_prod (s : Submonoid M) (t : Submonoid N) : (prod s ⊥) ⊔ (prod ⊥ t) = prod s t :=
  (le_antisymm (sup_le (prod_mono (le_refl s) bot_le) (prod_mono bot_le (le_refl t)))) fun p hp =>
    Prod.fst_mul_snd p ▸
      mul_mem ((le_sup_left : prod s ⊥ ≤ prod s ⊥ ⊔ prod ⊥ t) ⟨hp.1, Set.mem_singleton 1⟩)
        ((le_sup_right : prod ⊥ t ≤ prod s ⊥ ⊔ prod ⊥ t) ⟨Set.mem_singleton 1, hp.2⟩)

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