α : Type ?u.284505
β : Type ?u.284508
γ : Type ?u.284511
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
ι : Type u
g : ι → Ordinal
inst✝ : Nonempty ι
a : Ordinal
⊢ f (Ordinal.sup g) ≤ a ↔ ∀ (i : ι), (f ∘ g) i ≤ a
α : Type ?u.284505
β : Type ?u.284508
γ : Type ?u.284511
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
ι : Type u
g : ι → Ordinal
inst✝ : Nonempty ι
a : Ordinal
⊢ f (Ordinal.sup g) ≤ a ↔ Ordinal.sup (f ∘ g) ≤ a
rw [sup_le_iff]
α : Type ?u.284505
β : Type ?u.284508
γ : Type ?u.284511
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
ι : Type u
g : ι → Ordinal
inst✝ : Nonempty ι
a : Ordinal
⊢ f (Ordinal.sup g) ≤ a ↔ ∀ (i : ι), f (g i) ≤ a
α : Type ?u.284505
β : Type ?u.284508
γ : Type ?u.284511
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
ι : Type u
g : ι → Ordinal
inst✝ : Nonempty ι
a : Ordinal
⊢ f (Ordinal.sup g) ≤ a ↔ ∀ (i : ι), (f ∘ g) i ≤ a
simp only [comp]
no goals
α : Type ?u.284505
β : Type ?u.284508
γ : Type ?u.284511
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
ι : Type u
g : ι → Ordinal
inst✝ : Nonempty ι
a : Ordinal
⊢ f (Ordinal.sup g) ≤ a ↔ ∀ (i : ι), f (g i) ≤ a
rw [H.le_set' Set.univ Set.univ_nonempty g] <;>
simp [sup_le_iff]