of_subset

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#IsCofinalFor.of_subset

English

If s is contained in t, then s is cofinal in t.

Русский

Если s ⊆ t, то s ко-финальное в t.

LaTeX

$$$$ s \subseteq t \Rightarrow \operatorname{IsCofinalFor}(s,t). $$$$

Lean4

@[simp]
theorem of_subset (hst : s ⊆ t) : IsCofinalFor s t := fun a ha ↦ ⟨a, hst ha, le_rfl⟩

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

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

Разделы

Аффилиация

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