subset — Mathlib

English

Restriction of a strict order to a subset s is again a strict order.

Русский

Ограничение строгого порядка к подмножеству s снова является строгим порядком.

LaTeX

$$IsStrictOrder α (\\lambda a b, r a b ∧ a ∈ s ∧ b ∈ s)$$

Lean4

instance subset : IsStrictOrder α fun a b : α => r a b ∧ a ∈ s ∧ b ∈ s
    where
  toIsIrrefl := ⟨fun a con => irrefl_of r a con.1⟩
  toIsTrans := ⟨fun _ _ _ ab bc => ⟨trans_of r ab.1 bc.1, ab.2.1, bc.2.2⟩⟩

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