English
For any x and a Chain c of Part α, x ∈ ωSup c if and only if some x ∈ c (i.e. Part.some x ∈ c i for some i).
Русский
Для любого x и цепочки c из Part α, x ∈ ωSup c тогда и только тогда, когда some x ∈ c (то есть Part.some x ∈ c i для некоторого i).
LaTeX
$$$x \in \omegaSup c \iff \text{Part.some } x \in c$$$
Lean4
theorem mem_ωSup (x : α) (c : Chain (Part α)) : x ∈ ωSup c ↔ some x ∈ c :=
by
simp only [ωSup, Part.ωSup]
constructor
· split_ifs with h
swap
· rintro ⟨⟨⟩⟩
intro h'
have hh := Classical.choose_spec h
simp only [mem_some_iff] at h'
subst x
exact hh
· intro h
have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩
rw [dif_pos h']
have hh := Classical.choose_spec h'
rw [eq_of_chain hh h]
simp
