α : Type u_2
β : Type ?u.276922
γ : Type ?u.276925
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
ho : o ≠ 0
c : α
⊢ range (familyOfBFamily o fun x x => c) = {c}
α : Type u_2
β : Type ?u.276922
γ : Type ?u.276925
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
ho : o ≠ 0
c : α
⊢ (brange o fun x x => c) = {c}
rw [← range_familyOfBFamily]
no goals
α : Type u_2
β : Type ?u.276922
γ : Type ?u.276925
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
ho : o ≠ 0
c : α
⊢ range (familyOfBFamily o fun x x => c) = {c}
exact @Set.range_const _ o.out.α (out_nonempty_iff_ne_zero.2 ho) c