sup_ind

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#sup_ind

← MathLib Explorer

English

In a linear order, if p(a) and p(b) then p(a ∨ b).

Русский

В линейном порядке, если выполняются p(a) и p(b), то верно p(a ∨ b).

LaTeX

$$$p(a) \rightarrow p(b) \rightarrow p(a \vee b)$$$

Lean4

theorem sup_ind (a b : α) {p : α → Prop} (ha : p a) (hb : p b) : p (a ⊔ b) :=
  (IsTotal.total a b).elim (fun h : a ≤ b => by rwa [sup_eq_right.2 h]) fun h => by rwa [sup_eq_left.2 h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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