inclusion_le_inclusion — Mathlib

English

If s ⊆ t with s,t subsets of α carrying a partial order, then x,y ∈ s satisfy i_h x ≤ i_h y iff x ≤ y; similarly for strict order.

Русский

Если s ⊆ t и на s,t задан порядок, то i_h preserves order: x ≤ y ⇔ i_h(x) ≤ i_h(y).

LaTeX

$$$\forall x,y \in s,\ i_h(x) \le i_h(y) \iff x \le y.$$$

Lean4

theorem inclusion_le_inclusion [LE α] {s t : Set α} (h : s ⊆ t) {x y : s} : inclusion h x ≤ inclusion h y ↔ x ≤ y :=
  Iff.rfl

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