mem_Ici_Ioi_of_subset_of_subset — Mathlib

English

If Ioi(a) ⊆ s ⊆ Ici(a), then s is either Ici(a) or Ioi(a).

Русский

Если Ioi(a) ⊆ s ⊆ Ici(a), то s равно либо Ici(a), либо Ioi(a).

LaTeX

$$$$ Ioi(a) \\subseteq s \\subseteq Ici(a) \\Rightarrow s \\in \\{Ici(a), Ioi(a)\\} $$$$

Lean4

theorem mem_Ici_Ioi_of_subset_of_subset {s : Set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) :
    s ∈ ({Ici a, Ioi a} : Set (Set α)) :=
  by_cases (fun h : a ∈ s => Or.inl <| Subset.antisymm hc <| by rw [← Ioi_union_left, union_subset_iff]; simp [*])
    fun h => Or.inr <| Subset.antisymm (fun _ hx => lt_of_le_of_ne (hc hx) fun heq => h <| heq.symm ▸ hx) ho

Похожие утверждения