skeletonLT_mono — Mathlib

English

If m ≤ n then skeletonLT C m ⊆ skeletonLT C n; skeletonLT is monotone in n.

Русский

Если m ≤ n, то skeletonLT C m ⊆ skeletonLT C n; LT-скелеты возрастaют по аргументу.

LaTeX

$$$m\\le n\\ \\Rightarrow\\ skeletonLT(C,D;m)\\subseteq skeletonLT(C,D;n)$$$

Lean4

theorem skeletonLT_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : (skeletonLT C m : Set X) ⊆ skeletonLT C n :=
  by
  simp_rw [coe_skeletonLT]
  apply union_subset_union_right
  intro x xmem
  simp_rw [mem_iUnion, exists_prop] at xmem ⊢
  obtain ⟨l, lltm, xmeml⟩ := xmem
  exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩

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