exists₂ — Mathlib

English

If e2.BoundaryGE i2 holds, there exists i1 with ac.Boundary i1 i2.

Русский

Если e2.BoundaryGE i2, тогда существует i1 с ac.Boundary i1 i2.

LaTeX

$$$e_2.BoundaryGE(i_2) \Rightarrow \exists i_1,\ ac.Boundary(i_1,i_2).$$$

Lean4

theorem exists₂ {i₂ : ι₂} (h : e₂.BoundaryGE i₂) : ∃ i₁, ac.Boundary i₁ i₂ :=
  by
  obtain ⟨h₁, h₂⟩ := h
  obtain ⟨i₁, hi₁⟩ := ac.exists_i₁ (c.prev (e₂.f i₂)) (fun i₂' hi₂' => h₂ i₂' (by simpa only [← hi₂'] using h₁))
  exact ⟨i₁, by simpa only [hi₁] using h₁⟩

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