English
Dual variant: CovBy K L holds if and only if K < L and for all H,g, K ≤ H ≤ L and g ∉ H implies g ∈ L and H = K.
Русский
Дуальная версия: CovBy K L выполняется тогда, когда K < L и для всех H,g, где K ≤ H ≤ L и g ∉ H, тогда g ∈ L и H = K.
LaTeX
$$$ \\mathrm{CovBy}(K,L) \\iff K < L \\land \\forall H\\, g,\\ K \\le H \\to H \\le L \\to g \\notin H \\to g \\in L \\to H = K.$$$
Lean4
/-- Dual variant of `SetLike.covBy_iff` -/
theorem covBy_iff' {K L : A} : K ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K :=
by
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_
push_neg
rw [lt_iff_le_and_ne, lt_iff_le_not_ge, and_and_and_comm]
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
SetLike.not_le_iff_exists, ne_comm, implies_true]
