prod_eq_bot_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 = \bot \leftrightarrow (s = \bot \land t = \bot)$$$

Lean4

@[to_additive prod_eq_bot_iff]
theorem prod_eq_bot_iff {s : Submonoid M} {t : Submonoid N} : s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥ := by
  simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot', mker_inl, mker_inr]

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