baseEmbedding_le_sSupFun — Mathlib

English

For a directed nonempty set c, seed.baseEmbedding ≤ sSupFun hc.

Русский

Для направленного непустого множества c, базовое вложение ≤ sSupFun hc.

LaTeX

$$$seed.baseEmbedding ≤ sSupFun\\; hc$$$

Lean4

theorem baseEmbedding_le_sSupFun {c : Set (Partial seed)} (hnonempty : c.Nonempty) (hc : DirectedOn (· ≤ ·) c) :
    seed.baseEmbedding ≤ sSupFun hc := by
  obtain ⟨f, hf⟩ := hnonempty
  exact le_trans f.prop.baseEmbedding_le (le_sSupFun hc hf)

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