ι : Type ?u.5056
α : Type u_1
β : Type ?u.5062
r r' : α → α → Prop
s t : Set α
x y : α
h : WellFounded fun a b => r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
ι : Type ?u.5056
α : Type u_1
β : Type ?u.5062
r r' : α → α → Prop
s t : Set α
x y : α
h : WellFoundedOn t r'
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFoundedOn s r
rw [wellFoundedOn_iff] at *
no goals
ι : Type ?u.5056
α : Type u_1
β : Type ?u.5062
r r' : α → α → Prop
s t : Set α
x y : α
h : WellFounded fun a b => r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
exact Subrelation.wf (fun xy => ⟨hle _ _ xy.1, hst xy.2.1, hst xy.2.2⟩) h