English
If Ioo(a,b) ⊆ s ⊆ Icc(a,b), then s ∈ {Icc(a,b), Ico(a,b), Ioc(a,b), Ioo(a,b)}.
Русский
Если Ioo(a,b) ⊆ s ⊆ Icc(a,b), тогда s принадлежит одному из Icc(a,b), Ico(a,b), Ioc(a,b), Ioo(a,b).
LaTeX
$$$$ Ioo(a,b) \\subseteq s \\subseteq Icc(a,b) \\Rightarrow s \\in \\{Icc(a,b), Ico(a,b), Ioc(a,b), Ioo(a,b)\\} $$$$
Lean4
theorem mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {s : Set α} (ho : Ioo a b ⊆ s) (hc : s ⊆ Icc a b) :
s ∈ ({Icc a b, Ico a b, Ioc a b, Ioo a b} : Set (Set α)) := by
classical
by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
· refine Or.inl (Subset.antisymm hc ?_)
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right, diff_singleton_subset_iff,
insert_eq_of_mem hb] at ho
· refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
· rw [← Icc_diff_right]
exact subset_diff_singleton hc hb
· rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
· refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
· rw [← Icc_diff_left]
exact subset_diff_singleton hc ha
· rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
· refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
rw [← Ico_diff_left, ← Icc_diff_right]
apply_rules [subset_diff_singleton]
