anti

Mathlib.Order.Filter.Subsingleton

URI: https://scilib.ai/kg/mathlib#Filter.Subsingleton.anti

English

If hl : l.Subsingleton and hl' : l' ≤ l, then l'.Subsingleton.

Русский

Если hl: l.Subsingleton и hl' : l' ≤ l, то l'.Subsingleton.

LaTeX

$$$hl : l.Subsingleton,\ hl' : l' \le l \Rightarrow l'.Subsingleton$$$

Lean4

theorem anti {l'} (hl : l.Subsingleton) (hl' : l' ≤ l) : l'.Subsingleton :=
  let ⟨s, hsl, hs⟩ := hl;
  ⟨s, hl' hsl, hs⟩

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

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

Разделы

Аффилиация

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