instOrderBot — Mathlib

English

If μ.transpose ≤ ν, then μ ≤ ν.transpose.

Русский

Если μ транспонированная ≤ ν, то μ ≤ ν транспонированная.

LaTeX

$$$ \mu^{\top} \le \nu \Rightarrow \mu \le \nu^{\top}. $$$

Lean4

/-- The empty Young diagram is (⊥ : young_diagram). -/
instance : OrderBot YoungDiagram
    where
  bot :=
    { cells := ∅
      isLowerSet := by
        intro a b _ h
        simp only [Finset.coe_empty, Set.mem_empty_iff_false]
        simp only [Finset.coe_empty, Set.mem_empty_iff_false] at h }
  bot_le _
    _ := by
    intro y
    simp only [mem_mk, Finset.notMem_empty] at y

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