brange_bfamilyOfFamily' — Mathlib

English

For any ι with a well-order r, brange of bfamOfFamily' equals range f.

Русский

Для любого ι с хорошим порядком r brange bfamilyOfFamily' равен range f.

LaTeX

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

Lean4

@[simp]
theorem brange_bfamilyOfFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) :
    brange _ (bfamilyOfFamily' r f) = range f :=
  by
  refine Set.ext fun a => ⟨?_, ?_⟩
  · rintro ⟨i, hi, rfl⟩
    apply mem_range_self
  · rintro ⟨b, rfl⟩
    exact ⟨_, _, bfamilyOfFamily'_typein _ _ _⟩

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