prod_eq_top_iff — Mathlib

English

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

Русский

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

LaTeX

$$$ \forall {s : Submonoid M} {t : Submonoid N},\ s.prod t = \top \leftrightarrow (s = \top \land t = \top)$$$

Lean4

@[to_additive prod_eq_top_iff]
theorem prod_eq_top_iff {s : Submonoid M} {t : Submonoid N} : s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤ := by
  simp only [eq_top_iff, le_prod_iff, ← mrange_eq_map, mrange_fst, mrange_snd]

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