prod_eq_top_iff — Mathlib

English

For nonempty M and N, s.prod t = ⊤ if and only if s = ⊤ and t = ⊤.

Русский

Для непустых M и N верно: s.prod t = ⊤ тогда и только тогда, когда s = ⊤ и t = ⊤.

LaTeX

$$$[Nonempty\ M] [Nonempty\ N] \; {s : Subsemigroup M} {t : Subsemigroup N},\; s. prod\ t = \top \iff s = \top \land t = \top$$$

Lean4

@[to_additive prod_eq_top_iff]
theorem prod_eq_top_iff [Nonempty M] [Nonempty N] {s : Subsemigroup M} {t : Subsemigroup N} :
    s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤ := by simp only [eq_top_iff, le_prod_iff, ← srange_eq_map, srange_fst, srange_snd]

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