Skip to content

Commit f325d56

Browse files
kim-emclaude
andcommitted
fix: wrap long docstring line to satisfy 100-char limit
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 2b55904 commit f325d56

File tree

1 file changed

+3
-2
lines changed
  • Mathlib/Order/ConditionallyCompleteLattice

1 file changed

+3
-2
lines changed

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -433,8 +433,9 @@ lemma ciSup_eq_univ_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = s
433433

434434
/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
435435
`s` and `t` have the same supremum. This holds even when the sets may be empty or unbounded. -/
436-
@[to_dual /-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
437-
`s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded. -/]
436+
@[to_dual /-- When every element of a set `s` is bounded by an element of a set `t`, and
437+
conversely, then `s` and `t` have the same infimum. This holds even when the sets may be empty or
438+
unbounded. -/]
438439
theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α}
439440
(hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
440441
sSup s = sSup t := by

0 commit comments

Comments
 (0)