prod_eq_top — Mathlib

English

The product equals the top if and only if at least one factor is top: s ×ˢ t = ⊤ iff s = ⊤ or t = ⊤.

Русский

Произведение равно верхнему множеству тогда и только тогда, когда хотя бы один из факторов равен верхнему: s ×ˢ t = ⊤ ⇔ s = ⊤ или t = ⊤.

LaTeX

$$$ s \times^{\mathrm{S}} t = \top \iff s = \top \lor t = \top $$$

Lean4

@[simp]
theorem prod_eq_top : s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤ :=
  by
  simp_rw [SetLike.ext'_iff]
  exact prod_eq_empty_iff

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