instOrderBot — Mathlib

English

The finsubgraphs form an ordered set with a bottom element, namely the bottom subgraph ⊥, which is below every finsubgraph.

Русский

Множество конечных подграфов упорядочено по порядку, существует наименьший элемент ⊥, который лежит ниже любого подграфа.

LaTeX

$$⊥_{G.Finsubgraph} ≤ x \\,\\forall x ∈ G.Finsubgraph$$

Lean4

instance : OrderBot G.Finsubgraph where
  bot := ⟨⊥, finite_empty⟩
  bot_le _ := bot_le (α := G.Subgraph)

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