isBot_iff — Mathlib

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⟩

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