ι : Type u
f : ι → Ordinal → Ordinal
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
⊢ (¬∃ i, nfpFamily f a ≤ f i b) ↔ ¬nfpFamily f a ≤ b
ι : Type u
f : ι → Ordinal → Ordinal
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
⊢ (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b
rw [← not_iff_not]
ι : Type u
f : ι → Ordinal → Ordinal
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a
ι : Type u
f : ι → Ordinal → Ordinal
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
⊢ (¬∃ i, nfpFamily f a ≤ f i b) ↔ ¬nfpFamily f a ≤ b
push_neg
no goals
ι : Type u
f : ι → Ordinal → Ordinal
inst✝ : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal
⊢ (∀ (i : ι), f i b < nfpFamily f a) ↔ b < nfpFamily f a
exact apply_lt_nfpFamily_iff H