case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))

case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))

case hf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => f a) (s ∩ {a | p a})

case hg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => g a) (s ∩ {a | ¬p a})
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => if p a then f a else g a) s
apply ContinuousOn.if'
case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
rintro a ha
case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (f a))
case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
simp only [← hp a ha, ite_self]
case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ closure {a | p a}] a) (𝓝 (f a))
case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (f a))
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
no goals
case hpf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ closure {a | p a}] a) (𝓝 (f a))
exact hf a ⟨ha.1, ha.2.1⟩
case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
rintro a ha
case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (g a))
case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
simp only [hp a ha, ite_self]
case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (g a))
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
case hpg.intro.intro
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : ¬a ∈ interior {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
case hpg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
rcases ha with ⟨has, ⟨_, ha⟩⟩
case hpg.intro.intro
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : a ∈ closure ({a | p a}ᶜ)
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
case hpg.intro.intro
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : ¬a ∈ interior {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
rw [← mem_compl_iff, ← closure_compl] at ha
no goals
case hpg.intro.intro
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : a ∈ closure ({a | p a}ᶜ)
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
apply hg a ⟨has, ha⟩
no goals
case hf
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => f a) (s ∩ {a | p a})
exact hf.mono (inter_subset_inter_right s subset_closure)
no goals
case hg
α✝ : Type ?u.373923
β✝ : Type ?u.373926
γ : Type ?u.373929
δ : Type ?u.373932
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => g a) (s ∩ {a | ¬p a})
exact hg.mono (inter_subset_inter_right s subset_closure)