infsep_pos_iff_nontrivial

Mathlib.Topology.MetricSpace.Infsep

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

← MathLib Explorer

English

For Finset s, 0 < s.toSet.infsep iff s.toSet.Nontrivial.

Русский

Для Finset s: 0 < s.toSet.infsep тогда и только тогда, когда s.toSet.Nontrivial.

LaTeX

$$$\forall s:\mathrm{Finset}\,\alpha, 0 < s.toSet.infsep \iff s.toSet.Nontrivial$$$

Lean4

theorem _root_.Finset.infsep_pos_iff_nontrivial (s : Finset α) : 0 < (s : Set α).infsep ↔ (s : Set α).Nontrivial :=
  infsep_pos_iff_nontrivial_of_finite

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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