instRelHomClassNatSetLeSubset — Mathlib

English

A compact exhaustion is monotone: if m ≤ n, then K_m ⊆ K_n, i.e., the exhaustion is increasing.

Русский

Исчерпывание компактными множествами монотонно: если m ≤ n, то K_m ⊆ K_n.

LaTeX

$$$$m\le n\Rightarrow K_m\subseteq K_n.$$$$

Lean4

instance : RelHomClass (CompactExhaustion X) LE.le HasSubset.Subset where
  map_rel f _ _ h := monotone_nat_of_le_succ (fun n ↦ (f.subset_interior_succ' n).trans interior_subset) h

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