preCantorSet_antitone — Mathlib

English

Antitone preCantorSet (duplicate): The family {preCantorSet(n)} is decreasing in n: for m ≤ n, preCantorSet(n) ⊆ preCantorSet(m).

Русский

Антимонотонность предканторово множества (дубликат): множество {preCantorSet(n)} убывает по x.

LaTeX

$$Antitone preCantorSet$$

Lean4

theorem preCantorSet_antitone : Antitone preCantorSet :=
  by
  apply antitone_nat_of_succ_le
  intro m
  simp only [Set.le_eq_subset, preCantorSet_succ, Set.union_subset_iff]
  induction m with
  | zero =>
    simp only [preCantorSet_zero]
    constructor <;> intro x <;> simp only [Set.mem_image, Set.mem_Icc, forall_exists_index, and_imp] <;>
          intro y _ _ _ <;>
        constructor <;>
      linarith
  | succ m ih => grind [preCantorSet_succ, Set.image_union]

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