anti

Mathlib.Data.Set.Subsingleton

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

English

If t is subsingleton and s ⊆ t, then s is subsingleton.

Русский

Если t субоднозначно, и s ⊆ t, то s также субоднозначно.

LaTeX

$$$ ht : t.Subsingleton \to hst : s \subseteq t \Rightarrow s.Subsingleton $$$

Lean4

theorem anti (ht : t.Subsingleton) (hst : s ⊆ t) : s.Subsingleton := fun _ hx _ hy => ht (hst hx) (hst hy)

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

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

Разделы

Аффилиация

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