instNeBotConditionalOfNonemptyOfLeOfIsDirectedGe

English

If β is nonempty and directed both ways, then (conditional β).NeBot.

Русский

Если β непусто и существуют направления как снизу, так и сверху, тогда (conditional β).NeBot.

LaTeX

$$$[\\text{Nonempty }\\beta]\\;[IsDirected]_{\\le}\\;[IsDirected]_{\\ge}\\; (\\text{conditional }\\beta).\\NeBot$$$

Lean4

instance [Nonempty β] [IsDirected β (· ≤ ·)] [IsDirected β (· ≥ ·)] : (conditional β).NeBot :=
  ⟨by simp; infer_instance⟩

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