exists₁ — Mathlib

English

If e1.BoundaryLE i1 holds, there exists i2 with ac.Boundary i1 i2.

Русский

Если e1.BoundaryLE i1, тогда существует i2, такое что ac.Boundary i1 i2.

LaTeX

$$$e_1.BoundaryLE(i_1) \Rightarrow \exists i_2,\ ac.Boundary(i_1,i_2).$$$

Lean4

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

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