English
A detailed characterization of when the lexicographic embedding preserves the covering relation, in terms of first coordinates and second coordinates with IsMax/IsMin conditions.
Русский
Подробная характеристика того, когда лексикографное вложение сохраняет покрывающую связь, в терминах первых координат и вторых с условиями IsMax/IsMin.
LaTeX
$$$$ {a_1 a_2 : \alpha} {b_1 b_2 : \beta} :\ toLex(a_1,b_1) \;\⋖\; toLex(a_2,b_2) \iff (a_1=a_2 ∧ b_1 \⋖ b_2) ∨ (a_1 \⋖ a_2 ∧ IsMax(b_1) ∧ IsMin(b_2)). $$$$
Lean4
theorem toLex_covBy_toLex_iff {a₁ a₂ : α} {b₁ b₂ : β} :
toLex (a₁, b₁) ⋖ toLex (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂ :=
by
simp only [CovBy, toLex_lt_toLex, toLex.surjective.forall, Prod.forall, isMax_iff_forall_not_lt,
isMin_iff_forall_not_lt]
constructor
· grind
· rintro (⟨rfl, hb, h⟩ | ⟨⟨ha, h⟩, hb₁, hb₂⟩)
· refine ⟨.inr ⟨rfl, hb⟩, fun a b ↦ ?_⟩
rintro (hlt₁ | ⟨rfl, hlt₁⟩) (hlt₂ | ⟨heq, hlt₂⟩)
exacts [hlt₁.not_gt hlt₂, hlt₁.ne' heq, hlt₂.false, h hlt₁ hlt₂]
· refine ⟨.inl ha, fun a b ↦ ?_⟩
rintro (hlt₁ | ⟨rfl, hlt₁⟩) (hlt₂ | ⟨heq, hlt₂⟩)
exacts [h hlt₁ hlt₂, hb₂ _ hlt₂, hb₁ _ hlt₁, hb₁ _ hlt₁]
