le_chainSup — Mathlib

English

The chainSup function provides an upper bound for a chain of partial refinements.

Русский

Функция chainSup предоставляет верхнюю границу для цепи частичных уточнений.

LaTeX

$$$\text{le_chainSup}(hc, ne, hfin, hU)(v) = v \le chainSup c hc ne hfin hU$$$

Lean4

/-- `chainSup hu c hc ne hfin hU` is an upper bound of the chain `c`. -/
theorem le_chainSup {c : Set (PartialRefinement u s p)} (hc : IsChain (· ≤ ·) c) (ne : c.Nonempty)
    (hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite) (hU : s ⊆ ⋃ i, u i) {v} (hv : v ∈ c) : v ≤ chainSup c hc ne hfin hU :=
  ⟨fun _ hi => mem_biUnion hv hi, fun _ hi => (find_apply_of_mem hc _ hv hi).symm⟩

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