shiftr — Mathlib

English

Prepending an empty set to a compact exhaustion shifts indices by one: (K.shiftr).find x = K.find x + 1.

Русский

Добавление пустого множества в начало исчерпывания сдвигает индексы на единицу: (K.shiftr).find x = K.find x + 1.

LaTeX

$$$$ (K.shiftr).find(x) = K.find(x) + 1. $$$$

Lean4

/-- Prepend the empty set to a compact exhaustion `K n`. -/
def shiftr : CompactExhaustion X where
  toFun n := Nat.casesOn n ∅ K
  isCompact' n := Nat.casesOn n isCompact_empty K.isCompact
  subset_interior_succ' n := Nat.casesOn n (empty_subset _) K.subset_interior_succ
  iUnion_eq' := iUnion_eq_univ_iff.2 fun x => ⟨K.find x + 1, K.mem_find x⟩

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