supported_le_supported_iff — Mathlib

English

For any s,t, with [Nontrivial R], supported(R,s) ≤ supported(R,t) iff s ⊆ t.

Русский

Для любых s,t, когда R не тривиально, выполнено: supported(R,s) ≤ supported(R,t) эквивалентно s ⊆ t.

LaTeX

$$$$ \mathrm{supported}(R,s) \le \mathrm{supported}(R,t) \iff s \subseteq t \quad [\text{Nontrivial }R] $$$$

Lean4

@[simp]
theorem supported_le_supported_iff [Nontrivial R] : supported R s ≤ supported R t ↔ s ⊆ t :=
  by
  constructor
  · intro h i
    simpa using @h (X i)
  · exact supported_mono

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