α : Type ?u.373286
β : Type ?u.373289
γ : Type ?u.373292
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
H : ∀ (b : Ordinal), b < a → ∃ i, f i = b
h : mex f < a
⊢ False
α : Type ?u.373286
β : Type ?u.373289
γ : Type ?u.373292
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
H : ∀ (b : Ordinal), b < a → ∃ i, f i = b
⊢ a ≤ mex f
by_contra' h
no goals
α : Type ?u.373286
β : Type ?u.373289
γ : Type ?u.373292
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
a : Ordinal
H : ∀ (b : Ordinal), b < a → ∃ i, f i = b
h : mex f < a
⊢ False
exact mex_not_mem_range f (H _ h)