disjointed_le_id

Mathlib.Order.Disjointed

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

English

For every i, disjointed f i ≤ f i, i.e., disjointed ≤ id.

Русский

Для каждого i выполнено disjointed f i ≤ f i, то есть disjointed ≤ id.

LaTeX

$$$\forall f:\ (disjointed f) \le (id : (\iota \to \alpha) \to \iota \to \alpha).$$$

Lean4

theorem disjointed_le_id : disjointed ≤ (id : (ι → α) → ι → α) := fun _ _ ↦ sdiff_le

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

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

Разделы

Аффилиация

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