forall_le_mono — Mathlib

English

If s ≤ t in Colex and every element of t is ≤ a, then every element of s is ≤ a.

Русский

Если s ≤ t в Colex и каждый элемент t ≤ a, тогда каждый элемент s ≤ a.

LaTeX

$$$s \le t \,\land\, (\forall b \in t, b \le a) \Rightarrow (\forall b \in s, b \le a)$$$

Lean4

/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small. -/
theorem forall_le_mono (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b ≤ a) : ∀ b ∈ s, b ≤ a :=
  by
  rintro b hb
  by_cases b ∈ t
  · exact ht _ ‹_›
  · obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›
    exact hbc.trans <| ht _ hct

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