isTop_iff — Mathlib

English

An element (a, b) of α × β is top if and only if a is top in α and b is top in β.

Русский

Элемент (a, b) из α × β является верхней гранью тогда и только тогда, когда a — верхняя грань в α и b — верхняя грань в β.

LaTeX

$$$IsTop(x) \iff (IsTop(x_1) \land IsTop(x_2))$$$

Lean4

theorem isTop_iff : IsTop x ↔ IsTop x.1 ∧ IsTop x.2 :=
  ⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩

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