diag_mono

Mathlib.Data.Finset.Prod

URI: https://scilib.ai/kg/mathlib#Finset.diag_mono

English

The map s ↦ diag(s) is monotone: if s ⊆ t then diag(s) ⊆ diag(t).

Русский

Отображение s ↦ diag(s) монотонно: если s ⊆ t, то diag(s) ⊆ diag(t).

LaTeX

$$Monotone( diag )$$

Lean4

@[mono]
theorem diag_mono : Monotone (diag : Finset α → Finset (α × α)) := fun _ _ h _ hx =>
  mem_diag.2 <| And.imp_left (@h _) <| mem_diag.1 hx

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

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

Разделы

Аффилиация

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