isMin_iff

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#Prod.isMin_iff

English

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

Русский

Элемент (a, b) из α × β минимален тогда и только тогда, когда a минимален в α и b минимален в β.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru