English
The chainHeight of a set equals the supremum of the chainHeights of its coordinate-wise intersections with Ici intervals.
Русский
Цепная высота множества равна наибольшему нижнему пределу цепных высот его пересечений с интервалами типа Ici.
LaTeX
$$s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Ici i).chainHeight$$
Lean4
theorem chainHeight_image (f : α → β) (hf : ∀ {x y}, x < y ↔ f x < f y) (s : Set α) :
(f '' s).chainHeight = s.chainHeight :=
by
apply le_antisymm <;> rw [chainHeight_le_chainHeight_iff]
· suffices ∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, map f l' = l
by
intro l hl
obtain ⟨l', h₁, rfl⟩ := this l hl
exact ⟨l', h₁, length_map _⟩
intro l
induction l with
| nil => exact fun _ ↦ ⟨nil, ⟨.nil, fun x h ↦ (not_mem_nil h).elim⟩, rfl⟩
| cons x xs hx =>
intro h
rw [cons_mem_subchain_iff] at h
obtain ⟨⟨x, hx', rfl⟩, h₁, h₂⟩ := h
obtain ⟨l', h₃, rfl⟩ := hx h₁
refine ⟨x :: l', Set.cons_mem_subchain_iff.mpr ⟨hx', h₃, ?_⟩, rfl⟩
cases l'
· simp
· simpa [← hf] using h₂
· intro l hl
refine ⟨l.map f, ⟨?_, ?_⟩, ?_⟩
· simp_rw [isChain_map, ← hf]
exact hl.1
· intro _ e
obtain ⟨a, ha, rfl⟩ := mem_map.mp e
exact Set.mem_image_of_mem _ (hl.2 _ ha)
· rw [length_map]
