union — Mathlib

English

Let C be a family of binary-valued functions on I, and suppose I is linearly ordered with a well-founded order; let o be an ordinal with o IsSuccLimit and C is contained below o. Then the range of C equals the union, over all ordinals o′ with o′ < o, of the sets smaller(C, o′).

Русский

Пусть C — семейство функций I → Bool и I упорядочено линейно; пусть o — ординал, удовлетворяющий условию IsSuccLimit, и C содержится ниже o. Тогда образ множества C равен объединению по всем o′ < o множеств smaller(C, o′).

LaTeX

$$$\\operatorname{range}(C)=\\bigcup_{e:\\{o'\\;|\\;o'

Lean4

theorem union : range C = ⋃ (e : { o' // o' < o }), (smaller C e.val) :=
  by
  ext p
  simp only [smaller, range, Set.mem_iUnion, Set.mem_image, Set.mem_range, Subtype.exists]
  refine ⟨fun hp ↦ ?_, fun hp ↦ ?_⟩
  · obtain ⟨l, hl, rfl⟩ := hp
    rw [contained_eq_proj C o hsC, Products.limitOrdinal C ho] at hl
    obtain ⟨o', ho'⟩ := hl
    refine ⟨o', ho'.1, eval (π C (ord I · < o')) ⟨l, ho'.2⟩, ⟨l, ho'.2, rfl⟩, ?_⟩
    exact Products.eval_πs C (Products.prop_of_isGood C _ ho'.2)
  · obtain ⟨o', h, _, ⟨l, hl, rfl⟩, rfl⟩ := hp
    refine ⟨l, ?_, (Products.eval_πs C (Products.prop_of_isGood C _ hl)).symm⟩
    rw [contained_eq_proj C o hsC]
    exact Products.isGood_mono C (le_of_lt h) hl

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