English
For any α, r, and subset s, s.WellFoundedOn r is equivalent to the well-foundedness of the relation on α given by r together with the condition that both arguments lie in s.
Русский
Для любых α, r и подмножества s утверждение s.WellFoundedOn r эквивалентно тому, что на α хорошо основано отношение, заданное как r вместе с условием a,b∈s.
LaTeX
$$s.WellFoundedOn(r) \\iff WellFounded(λ a b:α, r a b ∧ a ∈ s ∧ b ∈ s)$$
Lean4
theorem wellFoundedOn_iff : s.WellFoundedOn r ↔ WellFounded fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
by
have f : RelEmbedding (Subrel r (· ∈ s)) fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s :=
⟨⟨(↑), Subtype.coe_injective⟩, by simp⟩
refine ⟨fun h => ?_, f.wellFounded⟩
rw [WellFounded.wellFounded_iff_has_min]
intro t ht
by_cases hst : (s ∩ t).Nonempty
· rw [← Subtype.preimage_coe_nonempty] at hst
rcases h.has_min (Subtype.val ⁻¹' t) hst with ⟨⟨m, ms⟩, mt, hm⟩
exact ⟨m, mt, fun x xt ⟨xm, xs, _⟩ => hm ⟨x, xs⟩ xt xm⟩
· rcases ht with ⟨m, mt⟩
exact ⟨m, mt, fun x _ ⟨_, _, ms⟩ => hst ⟨m, ⟨ms, mt⟩⟩⟩
