mem_chain_of_mem_ωSup — Mathlib

English

Let c be a Chain in Part α. If a ∈ Part.ωSup c, then some a is contained in the chain, i.e. there exists an index i with Part.some a ∈ c i.

Русский

Пусть c — цепочка в Part α. Если a ∈ Part.ωSup c, то некоторый элемент a присутствует в цепочке, т.е. существует индекс i, такой что Part.some a ∈ c i.

LaTeX

$$$a \in \ Part.ωSup(c) \Rightarrow \text{some } a \in c$$$

Lean4

theorem mem_chain_of_mem_ωSup {c : Chain (Part α)} {a : α} (h : a ∈ Part.ωSup c) : some a ∈ c :=
  by
  simp only [Part.ωSup] at h; split_ifs at h with h_1
  · have h' := Classical.choose_spec h_1
    rw [← eq_some_iff] at h
    rw [← h]
    exact h'
  · rcases h with ⟨⟨⟩⟩

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