range_familyOfBFamily' — Mathlib

English

The range of the primed reindexed family equals the brange of f.

Русский

Диапазон перерандексированного семейства равен brange f.

LaTeX

$$$\mathrm{range}(\mathrm{familyOfBFamily'}\ r\ ho\ f) = \mathrm{brange}(o,f)$$$

Lean4

@[simp]
theorem range_familyOfBFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o)
    (f : ∀ a < o, α) : range (familyOfBFamily' r ho f) = brange o f :=
  by
  refine Set.ext fun a => ⟨?_, ?_⟩
  · rintro ⟨b, rfl⟩
    apply mem_brange_self
  · rintro ⟨i, hi, rfl⟩
    exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩

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