English
Let f be normal. For a nonempty set p of ordinals and a bound o, if for all o the relation b ≤ o is equivalent to ∀ a ∈ p, a ≤ o, then f(b) ≤ o is equivalent to ∀ a ∈ p, f(a) ≤ o.
Русский
Пусть f — нормальная функция. Пусть p — непустое множество ординалов, и o — граница. Если для всех o верно: b ≤ o тогда и только тогда, когда ∀ a ∈ p, a ≤ o, тогда f(b) ≤ o эквивалентно ∀ a ∈ p, f(a) ≤ o.
LaTeX
$$$\forall f\,\bigl(\mathrm{IsNormal}(f)\bigr)\; \forall p\; (p\neq \emptyset)\; \forall b\; \forall o,\; \Bigl\{\; \Bigl(\forall o,\; b \le o \iff \forall a \in p, a \le o\Bigr) \Bigr\} \to \Bigl( f(b) \le o \iff \forall a \in p, f(a) \le o\Bigr).$$$
Lean4
theorem le_set {f o} (H : IsNormal f) (p : Set Ordinal) (p0 : p.Nonempty) (b) (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, a ≤ o) :
f b ≤ o ↔ ∀ a ∈ p, f a ≤ o :=
⟨fun h _ pa => (H.le_iff.2 ((H₂ _).1 le_rfl _ pa)).trans h, fun h => by
induction b using limitRecOn with
| zero =>
obtain ⟨x, px⟩ := p0
have := Ordinal.le_zero.1 ((H₂ _).1 (Ordinal.zero_le _) _ px)
rw [this] at px
exact h _ px
| succ S _ =>
rcases not_forall₂.1 (mt (H₂ S).2 <| (lt_succ S).not_ge) with ⟨a, h₁, h₂⟩
exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁)
| limit S L _ =>
refine (H.le_iff_forall_le L).2 fun a h' => ?_
rcases not_forall₂.1 (mt (H₂ a).2 h'.not_ge) with ⟨b, h₁, h₂⟩
exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)⟩
