exists_le_of_le — Mathlib

English

If P ≤ Q and b ∈ Q.parts, then there exists c ∈ P.parts with c ≤ b.

Русский

Если P ≤ Q и b ∈ Q.parts, существует c ∈ P.parts such that c ≤ b.

LaTeX

$${a,b} \text{ такие, что } P \le Q \Rightarrow \exists c\in P.parts: c \le b$$

Lean4

theorem exists_le_of_le {a b : α} {P Q : Finpartition a} (h : P ≤ Q) (hb : b ∈ Q.parts) : ∃ c ∈ P.parts, c ≤ b :=
  by
  by_contra H
  refine Q.ne_bot hb (disjoint_self.1 <| Disjoint.mono_right (Q.le hb) ?_)
  rw [← P.sup_parts, Finset.disjoint_sup_right]
  rintro c hc
  obtain ⟨d, hd, hcd⟩ := h hc
  refine (Q.disjoint hb hd ?_).mono_right hcd
  rintro rfl
  simp only [not_exists, not_and] at H
  exact H _ hc hcd

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