English
An element (a, b) of α × β is bottom if and only if a is bottom in α and b is bottom in β.
Русский
Элемент (a, b) из α × β является нижней гранью тогда и только тогда, когда a — нижняя грань в α и b — нижняя грань в β.
LaTeX
$$$\ IsBot(x) \iff (IsBot(x_1) \land IsBot(x_2))$$$
Lean4
theorem isBot_iff : IsBot x ↔ IsBot x.1 ∧ IsBot x.2 :=
⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩