English
An induction principle for sup' with bottom: if p is closed under binary sup and holds on each f(b) for b ∈ s, then p(s.sup' H f) holds.
Русский
Индукционное тождество для sup' с нулём: если свойство p сохраняется под бинарным объединением и верно для каждого f(b), то верно и для s.sup' H f.
LaTeX
$$$p(s.sup' H f)$, given the stated inductive conditions$$
Lean4
theorem sup'_induction {p : α → Prop} (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊔ a₂)) (hs : ∀ b ∈ s, p (f b)) :
p (s.sup' H f) := by
change @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)
rw [coe_sup']
refine sup_induction trivial (fun a₁ h₁ a₂ h₂ ↦ ?_) hs
match a₁, a₂ with
| ⊥, _ => rwa [bot_sup_eq]
| (a₁ : α), ⊥ => rwa [sup_bot_eq]
| (a₁ : α), (a₂ : α) => exact hp a₁ h₁ a₂ h₂
